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

The Case for Formal Verification (2013)

permalink.gmane.org

Post reply on HN
Print view View original

31–40 of 113 posts

Re: The Case for Formal Verification (2013)

#31

Post by betterunix »

Igglyboo wrote: post #9
cwzwarich wrote: post #8

Earlier quoted context omitted.

Even ignoring the licensing issues and limited subset of C supported, the code quality doesn't approach that of modern optimizing compilers, and the correctness proof doesn't include things like concurrency or actual machine memory models (although forks of CompCert exist for some of these), so you're still off in the unverified world if you rely on them in your code. Also, for the vast majority of programs the possi…

The article said something about being as good as GCC with O1, is that not enough? Pardon my ignorance, I've never touched c/c++ (python guy).

1. O3 is way better.

2. GCC is not even the best optimizing compiler out there. Intel's C compiler puts GCC to shame for some tasks.

Re: The Case for Formal Verification (2013)

#32

Post by anaphor »

Pacabel wrote: post #11
dkarapetyan wrote: post #2

Yes on all counts. I never understood why the TDD culture was happy to write down a complicated function and then only verify that on input 2 the output was 4. It always seemed backwards to me especially when you could have just as easily verified that in the REPL and called it a day. To me TDD on its own is just glorified documentation and tells me nothing about the actual properties of the software. Formal proofs a…

Your description of TDD is a pretty blatant misrepresentation of the actual philosophy and techniques. Furthermore, I think that you're ignoring that TDD tries to be a practical solution to certain real-world problems. This means that trade-offs are made in the name of creating software that works sufficiently well, while keeping expenses in check. Sure, extensive formal verification of all software would probably br…

The QuickCheck model is at least as good as unit tests and is more likely to actually find bugs and corner cases. The resulting code is no more complex either. The only drawback I see is that it requires you to design your code in a very modular way that makes things amenable to automated input generation.

Re: The Case for Formal Verification (2013)

#33

Post by 0x0 »

dkarapetyan wrote: post #2

Yes on all counts. I never understood why the TDD culture was happy to write down a complicated function and then only verify that on input 2 the output was 4. It always seemed backwards to me especially when you could have just as easily verified that in the REPL and called it a day. To me TDD on its own is just glorified documentation and tells me nothing about the actual properties of the software. Formal proofs a…

It can still be useful documentation. Four years later and after a couple rounds of heavy refactoring, it's nice to verify that 2+2 still equals 4.

Re: The Case for Formal Verification (2013)

#34

Post by jahewson »

comex wrote: post #23

Somewhat off topic and very speculative, but I'm curious how feasible it would be to propagate safety proofs through compilation - not just formulaic memory safety rules but hopefully also arbitrary behavioral proofs - all the way down from a source language to machine code, so that essential properties could be formally verified without needing to either trust a compiler or use a provably correct one, in the latter…

There's some academic work in this area under the name of "proof-carrying code": http://en.m.wikipedia.org/wiki/Proof-carrying_code

Re: The Case for Formal Verification (2013)

#35

Post by userbinator »

I think one of the biggest barriers to formal verification is that it is, for lack of a better term, "too formal". There's a bunch of other terminology, language, etc. you have to learn, and the learning curve is steep. For someone who just wants to prove a few pre/post-conditions on some functions (that's why I looked into Coq originally - and gave up because it was too hard), it's too much. There is a feeling that it is too theoretical. I eventually found it easier to prove what I needed to, manually.

Re: The Case for Formal Verification (2013)

#36

Post by jnbiche »

tluyben2 wrote: post #12
ramidarigaz wrote: post #3

Relevant: I attended LambdaConf yesterday at CU Boulder, and there was a _great_ intro workshop for Idris, which is in the same domain as Coq. Idris is similar to Haskell (it's actually written in Haskell), but with a dependent type system, a tactic-based theorem prover like Coq has, and a bunch of other fun features.

Idris is really worth checking out if you have any interest in this kind of stuff. I used Coq and now am playing with Idris and F*; the latter two feel good and practical. With an FP background they are easy to pick up.

I've also been playing around with these two. I have a little Haskell and some OCaml, but very little understanding of the mathmatics involved in dependent typing, so I'm struggling but still very interested. Wish there were an accessible guide like "Learn you a Haskell" for Idris.

By the way, for anyone interested in these two languages with dependent typing, you can try out both Idris and F* online, without installing anything:

http://www.tryidris.org/console

http://rise4fun.com/FStar/tutorial/guide

Re: The Case for Formal Verification (2013)

#37

Post by jnbiche »

userbinator wrote: post #35

I think one of the biggest barriers to formal verification is that it is, for lack of a better term, "too formal". There's a bunch of other terminology, language, etc. you have to learn, and the learning curve is steep. For someone who just wants to prove a few pre/post-conditions on some functions (that's why I looked into Coq originally - and gave up because it was too hard), it's too much. There is a feeling that…

Bingo, unfortunately. I've been able to learn functional programming in Haskell and OCaml without any formal academic background, but looking at Coq, Agda, Idris, and F*, I despair of learning them without more accessible tutorials or a PhD in computer science concentrating on type theory.

My first intro to Haskell was through "Learn you a Haskell". I think without that type of introduction, I never would have progressed past basic pattern matching and folds/maps/filters. I need something similar for dependent typing.

Re: The Case for Formal Verification (2013)

#39

Post by platz »

dkarapetyan wrote: post #2

Yes on all counts. I never understood why the TDD culture was happy to write down a complicated function and then only verify that on input 2 the output was 4. It always seemed backwards to me especially when you could have just as easily verified that in the REPL and called it a day. To me TDD on its own is just glorified documentation and tells me nothing about the actual properties of the software. Formal proofs a…

Perhaps Test Driven Design is more about producing a certain kind of design, rather than about guarantees about correctness.

Re: The Case for Formal Verification (2013)

#40

Post by stormbrew »

dkarapetyan wrote: post #2

Yes on all counts. I never understood why the TDD culture was happy to write down a complicated function and then only verify that on input 2 the output was 4. It always seemed backwards to me especially when you could have just as easily verified that in the REPL and called it a day. To me TDD on its own is just glorified documentation and tells me nothing about the actual properties of the software. Formal proofs a…

I find it strange to think that TDD and formal verification are at odds with each other. For it to be backwards to write dynamic tests, you seem to be suggesting that it is actually worse than doing neither. I also don't see how it can be documentation, glorified or otherwise, and not tell you anything about the properties of the software.

Really there are perhaps three practical levels of knowledge about what a piece of code does: - It does something. - If I give it X it gives me Y (for some finite set of X). - It will never do Z (for some finite set of Z).

The first is the state most software is in most of the time. The second is achievable with tests and some kinds of static analysis. The last is probably only achievable with formal analysis and code that fits the constraints of that formal analysis.

But both levels are at least an improvement on nothing at all. Having functional and documenting tests does bring meaningful knowledge about some subset of what the code does, even if it isn't the be-all and end-all of code analysis.

So I don't see how you can dismiss it so easily, when to me it's just a step on that striving you mention in your final sentence. For the moment it is perhaps true that the good is the enemy of the great on this, but that will become less true as the tools get better.

After all, even this article talks about only formally verifying part of the code of a web browser. Until and unless formally verifying the entire thing becomes possible, you still probably need the Acid tests to demonstrate its capabilities and help prevent regression.

Post reply on HN