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

161–170 of 232 posts

Re: Why Don't People Use Formal Methods?

#161

Post by mbrock »

zanny wrote: post #5

I think it goes beyond conservatism for most devs as to why you don't formally specify your design and its mostly rooted in why AGILE is so popular. The sooner you show a finished product, no matter how broken and incomplete, the sooner your client can realize all the things they didn't want they said they did and replace them. If you give them a formal design document it might be ironclad and foolproof but it doesn'…

Thorough automatic testing is valued by agile practitioners because it lets them move faster even thought it might initially seem like more testing means more work means slower iterations. I think a similar effect is possible when you use specification languages and model checkers as part of an agile way of working. The spec is at a higher level than the implementation and hopefully radically shorter and easier to adapt. The model checker then lets you find flaws in design changes faster than you would have without it.

Re: Why Don't People Use Formal Methods?

#162

Post by amelius »

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…

> The really simple answer to this question is: because at a high level of abstraction, it isn't useful.

Okay, but if you're implementing a complicated algorithm like Paxos or Draft, then it can be useful to put some assertions in your code, and prove them in a formal language; and also to make these proofs part of the unit tests.

Re: Why Don't People Use Formal Methods?

#163

Post by iso-8859-1 »

dranov wrote: post #135
xiphias2 wrote: post #41

Bitcoin is at a point in valuation where a huge effort should be put into using formal verification: a bug can worth hundreds of billions of dollars. One problem is that it's already written in C++, which is a language with incredibly complex semantics for program verification (and now it's too hard to move away, so the C++ program has to be proven to be correct). The main blocker is what others have written as well:…

I agree, and there are efforts to develop formally verified implementations of Nakamoto consensus (which I'm involved in). We've published a paper a year ago about our efforts and first results and I'm currently extending that work for my Master's thesis. Others are also building on top of that work [3]. We're nowhere near having a verified Bitcoin implementation (much less verifying the existing C++ implementation),…

First you mention Nakamoto consensus, then you mention "existing consensus code". Are you including Bitcoin script when you say consensus? It seems like a huge task to formally model the whole consensus system, including OP_CODESEPARATOR. How would you replicate something like the BIP-0050 problem?

https://github.com/bitcoin/bips/blob/master/bip-0050.mediawi...

Re: Why Don't People Use Formal Methods?

#164

Post by kiriakasis »

Silhouette wrote: post #97
cryptica wrote: post #93

Earlier quoted context omitted.

Completely agree. This line sums it up: >> Before we prove our code is correct, we need to know what is “correct”. This means having some form of specification That is the problem. The people who come up with the spec don't fully know what is required. It's even worse than that actually; the requirements change constantly to account for changes in the technological and business environment within which the project ex…

The people who come up with the spec don't fully know what is required. It's even worse than that actually; the requirements change constantly to account for changes in the technological and business environment within which the project exists. I think this is a bit of an overstatement, because it implies an often unrealistic separation between writing specs and writing implementations. There may be several levels of…

> it implies an often unrealistic separation between writing specs and writing implementations

I think that part of the problem is that small modification in the spec can lead to enormous changes in the proofs

Re: Why Don't People Use Formal Methods?

#165

Post by jononor »

pytester wrote: post #123
cryptica wrote: post #93

Earlier quoted context omitted.

Completely agree. This line sums it up: >> Before we prove our code is correct, we need to know what is “correct”. This means having some form of specification That is the problem. The people who come up with the spec don't fully know what is required. It's even worse than that actually; the requirements change constantly to account for changes in the technological and business environment within which the project ex…

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…

Would the code have been as clean and clear if you did not make the formal spec beforehand?

Re: Why Don't People Use Formal Methods?

#166

Post by alexisread »

ummonk wrote: post #122
twblalock wrote: post #26

Formal methods don't make a lot of sense when the product changes from week to week, or month to month, or even year to year. It seems like the advocates of formal methods assume a waterfall method of software development wherein you develop a spec, formalize it, prove that it works, and then deliver it. That's just not how software works in industry. A lot of it never had formal specs and never will, and whatever sp…

I'm not sure that is necessarily true. I think of the modern typechecker (especially with generics, algebraic data types, and other advanced features, including sometimes dependent tpes) as basically formal-verification-lite, and it tends to work really well with changing specs. You can aggressively refactor and change code and just let the compiler catch errors as you go. A practical formal verification language wou…

This! I'd also argue that your formal verification language and your coding language are one and the same. This leads to the case where if you can specify your language, it is written. Obviously there are scenarios where it's not practical to prove a part of the program, but you can simply use an unsafe dialect as per Rust or Maude (system modules).

This works well with agile development in that you can spec out the underlying communications protocols, parallel operations etc. and layer unsafe stuff on top. While we're here then, being able to publish these proven modules for other people should lead to a situation where we can build incrementally on code proofs.

Lastly, you can consider this system to be the equivalent of unit tests, but better in that there are guaranteed to be no edge cases you haven't tested (subject to coverage, but again publishing modules should help bullet-proof them). For integration testing, you can use behavioural proofs - see Maude or BOBJ.

Re: Why Don't People Use Formal Methods?

#167

Post by Nokinside »

I have used statistical analysis and formal methods in production code. Mainly Astree, https://www.absint.com/astree/index.htm

When you have bought the tools to verify code in some safety critical project and know how to use it, it's easier to use it in less critical software too. You will soon hit the wall where formal correctness loses to time constraints and new features. You end up verifying only the code that is used repeatedly in multiple projects and does not change.

Formal verification is not substitute for testing and code review. You can verify that the code is correct but you don't know if you have the correct code.

The answer is: Because correctness of programs produces only limited value for normal use cases. It's more important to add more features than it is to produce solid code. If you don't have code reviews where all new code and changes are being read and analyzed by others (increasing the cost of the software 5-10 times) your interest in correct code is limited.

Re: Why Don't People Use Formal Methods?

#168

Post by kiriakasis »

microcolonel wrote: post #124
cryptica wrote: post #93

Earlier quoted context omitted.

Completely agree. This line sums it up: >> Before we prove our code is correct, we need to know what is “correct”. This means having some form of specification That is the problem. The people who come up with the spec don't fully know what is required. It's even worse than that actually; the requirements change constantly to account for changes in the technological and business environment within which the project ex…

I think the issue with the way people try to promote the use of formal methods, is that they assume that people will want to model their system formally before implementing it. I feel like there'd be more productivity in showing people what their code could do, and helping them narrow that down to what it should . It is, of course, hard to do this.

From this point of view I like TLA+, it gives you a simple but powerful programming language and then allows you to check stuff like "this must not happen" or "this must happen" (and more).

Formal proof as in coq-proof are often not reasonable for many dynamic projects

Re: Why Don't People Use Formal Methods?

#170

Post by namelosw »

The main reason is formal method is still not cost-efficient, not even close.

The problem is similar to statically typed languages. Of course, having a sound type system can help you avoid a lot of stupid mistakes. But the key point of modern statically typed language does not lose a lot of velocities. Sometimes even faster because there are better IDEs out there for auto-completion, importing, and much other stuff. I switched from JavaScript to TypeScript only to find I'm faster to write code without losing anything.

Before we make formal method widely accepted by the industry, we probably need depdent type languages first. An excellent example is Idris. https://www.idris-lang.org/ It's a dependent type language, and it can also apply formal method to prove theorems. With its IDE, it is more like pair programming with the type system, it can really fill up a lot of code according to type. This kind of system could have huge potential to be much more powerful than say, IntelliJ IDEA with Java etc.

After then you could write code very faster, you could optionally write some proof for the core domain of your system if you like.

Post reply on HN