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

51–60 of 113 posts

Re: The Case for Formal Verification (2013)

#51

Post by dkarapetyan »

jarrett wrote: post #50

Will formal verification ever be possible for systems composed of a bunch of heterogeneous components working together? I'm thinking of a web application, where the software's behavior depends on the interaction of client-side scripts, stylesheets, server-side programs, databases, caching layers, and probably other components, all operating in the request-response cycle that fragments behavior into a bunch of separat…

Why not? Each of those things can be treated as black boxes with well-defined interfaces.

Re: The Case for Formal Verification (2013)

#52

Post by CHY872 »

ryanobjc wrote: post #18
noselasd wrote: post #10

Earlier quoted context omitted.

One big advantage is regression testing - which is why you don't just test it in a REPL and forget about it.

Totally agree here, manually verifying a chunk of code once, for example early on in the dev lifecycle, then having it exist inside a big system is really the "EE" way of doing things. But the reality is you gotta dig deep and change stuff, after all how often does an engineer dive in and change how a transistor works (laws of physics be damned!) I feel like overall software quality has been harmed by the emphasis of…

I'm sorry, but I don't believe this point has any merit with regards to this discussion. Formal verification was seen as the future for large systems for some short time in the latter half of the 20th century, and since then no one has seriously suggested verifying programs of millions lines of code. The point that is made here (quite sensibly) is that in many cases, by verifying small parts of your codebase (a few hundred lines, perhaps), you can rule out whole classes of bugs.

To give some useful real-life exampled, in OCaml (or at least in Standard ML), if a program compiles one can know that it will never crash (i.e. leave the control of the system - it might still abort) unless the compiler has a bug (and there's now a verified ML compiler for x64). Other useful properties might be to prove that a driver terminates (Microsoft SLAM/T2) and so will never hang the system, or a compiler that produces code semantically equivalent to the spec of the language.

You say that software quality has been harmed by the emphasis of mathematical proof of code - I just don't see how this can be the case. In a typical education, a student will see two types of proving code - in an algorithms class, where it is required in order to show that the algorithm solves the problem (and totally separately to actually building software systems), and in the formal verification/model class, which I doubt is taught at many universities and is almost certainly optional.

If someone enters the workforce without sufficient knowledge of test driven development, isn't taught at their place of work and writes bad code, there's a nice long list of people they can blame (their bosses, the people reviewing their code, their style book, their examiners, their lecturers, etc.) but it's not valid to blame formal verification for this, no more than it is valid to blame the hypothetical course on FPGA programming they took at some point.

Yes, test driven development is great, but it is totally complementary to this sort of thing.

Re: The Case for Formal Verification (2013)

#53

Post by hyp0 »

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…

More like glorious documentation: verified to be up to date... and has examples.

As others mentioned, regression testing is about the only really useful correctness step. There's also motivation, to keep on track for what is actually needed. Also it helps you write an API, rather than just implementation: the tests are a client. (On the downside, these extra clients depedence on your API, also make it more work to change that interface, giving it more inertia). Plus: who shall test the tests?

NB: I'm not a TDD adherent, never used it, so take what I say with a grain of salt: it's just my own reasoning + what I've heard from people who've tried it.

Re: The Case for Formal Verification (2013)

#54

Post by [deleted] »

anaphor wrote: post #32
Pacabel wrote: post #11

Earlier quoted context omitted.

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.

[deleted]

Re: The Case for Formal Verification (2013)

#55

Post by gsnedders »

rossjudson wrote: post #29
wsxcde wrote: post #24

Coq is an interactive theorem-prover, which is exactly what it sounds like. You prove your theorems more or less by typing out the proofs and the system mechanically verifies that each step in your proof is sound. I've used Coq and I'll be honest. This is unquestionably a solid way to prove things about your program but it is too much of pain to expect this to have significant adoption in the "real" world. In the har…

I get what you're saying about the state explosion problem, but the article specifically calls out the idea of proving a lack of negative behaviors. It seems to me it might be quite useful to be able to prove, for example, that a program never reads memory at random, or that it never exceeds the bounds of any allocated buffer. That's a different problem scale than "prove the whole thing works as specified".

Sadly, it's not a different problem scale — the typical model is something similar to "for each state, does the property P hold?". Hence no matter the property (or complexity thereof), one must still enumerate all states.

Re: The Case for Formal Verification (2013)

#56

Post by gsnedders »

jarrett wrote: post #50

Will formal verification ever be possible for systems composed of a bunch of heterogeneous components working together? I'm thinking of a web application, where the software's behavior depends on the interaction of client-side scripts, stylesheets, server-side programs, databases, caching layers, and probably other components, all operating in the request-response cycle that fragments behavior into a bunch of separat…

Certainly — it's just another parallel system. This is something things like CSP (Communicating Sequential Processes) — and see FDR2/FDR3 for programmatic verification — excel at.

Re: The Case for Formal Verification (2013)

#57

Post by gsnedders »

jnbiche wrote: post #37
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 progre…

There's Learn You An Agda at " rel="nofollow">https://github.com/liamoc/learn-you-an-agda>, though it never got that far. (I've done comparatively little with theorem provers (v. model checkers), so I can't point you anywhere that useful!)

Re: The Case for Formal Verification (2013)

#58

Post by solomatov »

gsnedders wrote: post #57
jnbiche wrote: post #37

Earlier quoted context omitted.

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 progre…

There's Learn You An Agda at " rel="nofollow">https://github.com/liamoc/learn-you-an-agda> , though it never got that far. (I've done comparatively little with theorem provers (v. model checkers), so I can't point you anywhere that useful!)

All these tutorials won't teach you how to use coq or agda. The main problem is that in order to use coq or agda, you need to learn Martin-Lof type theory (or calculus of inductive constructions, which is a similar formalism to MLTT) first, and learn to write code later. Otherwise everything will seem like a magic. There are however, good books on the topic:

* Type Theory and Functional Programming (http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/)

* Programming in Martin-Lof type theory (http://www.cse.chalmers.se/research/group/logic/book/)

Re: The Case for Formal Verification (2013)

#59

Post by munin »

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…

you might be interested in this work: http://research.microsoft.com/pubs/176601/js-star.pdf

Re: The Case for Formal Verification (2013)

#60

Post by sanxiyn »

ryanobjc wrote: post #21
daleharvey wrote: post #15

Earlier quoted context omitted.

Really confused at why this comment is being so harshly downvoted, it seems fairly accurate, possibly downplaying how useful formal verification may be in the future, but the parent is most definitely misrepresenting the practicality and usefulness of TDD

I also agree, have some upboats. The reality is that programming is an engineering endeavor, and in the face of limited resources, we have to choose the tools that can offer realistic benefits now. Formal verification is not that tool for most projects right now. Would instagram or even facebook be better off? Most people would, correctly, say no. And ultimately in the end, nearly all software (including quite a bit…

I'd think the security of Facebook privacy settings will be improved by, for example, lightweight modelling using Alloy. Alloy would catch bugs like this one:

http://mashable.com/2011/12/06/facebook-bug-zuckerberg-photo...

When I read about that bug in the past, I thought "this would be a great example to use for Alloy".

Post reply on HN