Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Why Don't People Use Formal Methods?

hillelwayne.com

Post reply on HN
Print view View original

151–160 of 232 posts

Re: Why Don't People Use Formal Methods?

#151

Post by bronsa »

TheFattestNinja wrote: post #140
tanilama wrote: post #129

If you want certain technology to be commercially successful, it needs to provide value. For the most part, most code are tolerated to be buggy, in exchange of fast delivery. And for most internet applications, a single error has limited scope, so the damage is controlled. For those applications, former methods are not something that could help them succeed, they don't even write a lot of unit tests. However, in diff…

Can you give me more examples of FM used in finance? I feel like they should be used, but in my limited experience with finance-related gigs I've been aghast at the lack of even basic testing put in place...

At Imandra (https://www.imandra.ai/) we've been collaborating with a few big names in finance, from our website: "In 2017 Aesthetic Integration partnered with Goldman Sachs to help deliver the SIGMA X MTF Auction Book, a new orderbook venue implementing periodic auctions. Aesthetic Integration used Imandra, our own automated reasoning engine, to formally model the Goldman Sachs design of the SIGMA X MTF Auction Book, verify its key properties, and automate rigorous testing. Now that the venue is live, Imandra is being used to perform ongoing validations of trading operations."

Re: Why Don't People Use Formal Methods?

#152

Post by roenxi »

majewsky wrote: post #139
roenxi wrote: post #115

Earlier quoted context omitted.

Well, yes, but if mathematicians prove something then we know it is true. And if they can't prove the trivialities, that would be a crisis for the entire discipline, because 1+1=2 relates to everything they do. If software people prove something we also know it is true, but not that it usefully relates to the software. In fact, 0.1+0.2 is likely != 0.3 for most software. You can prove you have integer types or fracti…

> You can prove you have integer types or fractional types or whatever, then a hardware bug comes along and your proof doesn't relate to the real world anyway. Proofs always rely on some sort of axiomatic system. Otherwise you don't have any basis for starting deductions. In most cases "the hardware conforms to its spec" can be considered a reasonable axiom (unless maybe in space flight where cosmic rays may cause ap…

This is fundamentally a complaint about some fairly specific language use. A lot of articles I've seen talking about formal methods contain some varient of "rigorously verified the correctness [of the program]". Anyone who is half-unsure about what is happening is going to write that off, because we all know programs can't be formally verified as correct in the common meaning of 'correct' because bugs are everywhere, at every level of the stack, and what people ask for probably isn't what they wanted anyway.

That is an abuse of language. What is happening is (and this is a good article because it is quite clear on the point) that "We’re ... prov[ing] ... conform[ance] to some spec.".

Now I'm quite excited at the prospect of automatic checking of conformance against a spec. Looking foward to the non-alpha release of spec in Clojure, in fact. But I'm going to ignore anyone who talks about "proving correctness" on the assumption that they (a) can't prove a program is correct in the abstract, (b) sound pretentious and (c) I'd be worried they are more worried about proving things than scoping and testing which is where most of the value sits.

Basically, I'm not saying formal methods are bad; quite the contrary; but the word 'proof' is not a safe word. It means very different things to different people. Most people outside software would surely assume bugs in the spec disprove 'correctness', but that isn't what the language seems to mean to formal methods people.

> the hardware conforms to its spec

Not a safe assumption. Spectre and Meltdown happened just last year; and I assume caused a lot of programs which were required to be high-certainty to become uncertain in practice.

The Software Engineering implications of a 'proof' are _different_ from a mathematician's standard of proof. If a mathematician uses a prooved fact, as long as the proof is correct then they have certainty. If an engineer uses a prooven program, they still don't have certainty because they are working in the real world.

I've opened news.ycombinator.com in firefox quite a few times over the years; every time I've either gotten the web page or a network error. That is a proof of correctness to the standards of 90% of the academic disciplines.

Re: Why Don't People Use Formal Methods?

#153

Post by brazzy »

mpweiher wrote: post #136
pytester wrote: post #123

Earlier quoted context omitted.

I think it's worse than that. I did a course on formal methods at university. The 'spec' ended up being a lot more complicated than the actual program. I wasn't really confident afterwards that the "proved" software actually did work. I think it's possibly a suitable method for building very low level code (e.g. sorting methods) where the spec is going to be exceptionally simple but it's effectiveness drops off quick…

I had exactly the same experience. We did specification in Z, but the code that was supposed to be "proved" correct was a clearer reflection of what we wanted to do than the "spec". So I actually had more confidence in the code than I did in the spec. And I think this answers the question of the OP: people don't use formal methods because (a) the vast majority of problems don't start out with a formal spec (b) the ga…

> And I think this answers the question of the OP

Do you realize that the OP is actually linking to an article explaining this (and a bunch of other aspects) in great detail?

Re: Why Don't People Use Formal Methods?

#154

Post by contravariant »

jpollock wrote: post #3

I've always wondered how I can write a specification in a language which is complex enough to cover the problem, clear enough to be verified by the customer, and not have it be as complex as writing the code.

If I could write a specification that satisfied all those properties I'd be happy if it was even remotely as simple as writing the code.

Re: Why Don't People Use Formal Methods?

#155

Post by verinus »

Jtsummers wrote: post #59
chubot wrote: post #55

Earlier quoted context omitted.

I think you're making a good point, but your tone is unnecessarily strident.

I'll disagree, I don't think they're making a good point. GP implies that formal methods always add time to projects, which is going to be true for: 1) Projects that are building the wrong thing and spend time verifying the wrong thing (failed validation) 2) Projects with people inexperienced in formal methods (most projects today) The latter is just a matter of experience. Once people get used to thinking about thin…

well if I read you correctly he IS making a good point:

> 2) Projects with people inexperienced in formal methods (most projects today)

which is exactly what matters and what adds a lot of time to dev.

1) cannot be addressed by formal method and is one of the most important things when building software.

Re: Why Don't People Use Formal Methods?

#157

Post by pron »

blub wrote: post #116
xvilka wrote: post #45

Part of the problem is that TLA+ syntax and tooling is horrendous. Creating something more modern and widely adoptable is a key for Mass scale applications.

TLA+ is an ugly language, just like PlusCal. I'll never understand how people can come to the conclusion that it's fine to have syntax like: * \A p \in people * acc = [p \in people |-> 5] * ( -- ; ) for wrapping PlusCal * /= for inequality * /\ for and * seq1 \o seq2 for append * and so on All of these are from the Practical TLA+ book. Honestly, TLA+ (or PlusCal) looks very impractical. If I want to use mathematical…

That's not the syntax, that's just the ASCII representation. The syntax, which is what you get when the Toolbox presents your spec in pretty-printed form, is:

  * ∀ p ∈ people
  
  * acc = [p ∈ people ↦ 5]

  * ≠ for inequality

  * ∧ for and

  * seq1 ∘ seq2 for append
That's fairly standard mathematical notation. In fact, one of the things I enjoyed about TLA+ is that I didn't really need to learn the syntax, as it's so standard. Even the non-standard bits (like alignment that can replace parentheses) are quite intuitive.

And if you say, well, I still have to type the ASCII, then you're missing the point. Specifications are not internet rants where you dump a lot of characters on the screen. They are usually quite short, and you spend nearly all your time thinking or reading them.

Re: Why Don't People Use Formal Methods?

#158

Post by pron »

mikekchar wrote: post #53

The really simple answer to this question is: because at a high level of abstraction, it isn't useful. Most applications are being specified by people who don't understand in any detail what they want the application to do. They can't even imagine the problem well enough to discuss it let alone specify it. A very large proportion of failed projects I've seen is due to this break down. The people who have the time and…

I think you're mistaking the use of formal methods for some particular process (like confusing tests with TDD). Formal methods do not require that you have a specification in advance. They can help you come up with the specification, through interaction, before or during coding (e.g., this is a lightweight formal specification tool for designing UIs and interaction: https://sketch.systems/).

As code is itself a specification at a very low level, you must have some kind of specification in your mind by the time you write it. Is it always worthwhile writing it in some formal methods tool? No, but it certainly can be when there is some subtlety or potential complication, which can arise even in seemingly simple programs. The author of this post has some nice examples here: https://youtu.be/tfnldxWlOhM

It is true that formal methods only help; they don't solve all of your problems, and they certainly can and do result in wrong specifications (e.g. KRACK attack and Spectre/Meltdown are examples of a wrong specification), but that doesn't mean they cannot be extremely helpful, just as unit tests are helpful even if they don't find all bugs.

Re: Why Don't People Use Formal Methods?

#159

Post by dmitriid »

agumonkey wrote: post #130
dmitriid wrote: post #117

Earlier quoted context omitted.

> Probably rejected willingly even ('where are my objects?') Local type inference was rejected in Java in 2001 because "you need to spec your types precisely"

is it published online ?

Found it here: https://stackify.com/whats-new-in-java-10/

——— start quote ———

This feature has been a long time coming. It was suggested as far back as 2001, and was closed at that time with the following comment by Gilad Bracha:

Humans benefit from the redundancy of the type declaration in two ways. First, the redundant type serves as valuable documentation – readers do not have to search for the declaration of getMap() to find out what type it returns. Second, the redundancy allows the programmer to declare the intended type, and thereby benefit from a cross-check performed by the compiler.

——— end quote ———

Link to original RFE and quote source: https://bugs.java.com/bugdatabase/view_bug.do?bug_id=4459053

Re: Why Don't People Use Formal Methods?

#160

Post by mbrock »

phtrivier wrote: post #121

I might be missing something obvious, but from my (small) reading about TLA+ (and the lamport video course), my biggest concerns were: A: even if you understand the spec you want to write, it's possible to get the implementation of the spec in the spec language wrong (see the Die Hard exercise in the course) ; isn't there some kind of recursive catch-22 there ? B: even if you understand the spec you want to write, an…

There’s a huge misunderstanding that pops up in every discussion about “formal methods.”

These methods are not perfect silver bullets to guarantee bug-free software forever. They are supposed to be useful engineering tools that help you think and verify your thinking especially for tricky corner cases and interactions.

So then it’s a bit like “Why would I think about the code I’m going to write when I could later make a mistake in implementing what I though?” Well, even so it has advantages over not thinking.

Not to suggest that “formal methods” are the only way of thinking. They’re just not really what people imagine they are when they criticize them.

Post reply on HN