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

61–70 of 113 posts

Re: The Case for Formal Verification (2013)

#61

Post by wsxcde »

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".

Model checking deals with two kinds of properties - safety and liveness. Safety properties effectively say nothing bad ever happens while liveness properties say that something good will eventually happen. For example, "my program will never crash due to a null point dereference" is a safety property. "My arbiter module will output a grant for every input request" is a liveness property.

It is true that model checkers are much better are proving safety properties than liveness properties. I think it's not too far from the truth to say that model checkers are no good at proving liveness properties in real designs and that only safety properties work (somewhat well) in practice.

An alternative here is to abandon model checking altogether and focus on a powerful static analysis. I think the main challenge here is coming up with effective property specification schemes. A powerful type system like Haskell does in fact enable you to prove quite strong statements about your program. But you are inherently limited in terms of what you can prove to whatever it is that the type system can express. To me, it seems that model checkers allow more flexibility in specifying your property, especially when you take into account the fact that you can do your model checking on an augmented/instrumented version of your design.

> That's a different problem scale than "prove the whole thing works as specified".

On a vaguely related note, equivalence checking between designs, especially in the hardware context, is one thing that formal tools have had a lot of success with.

Re: The Case for Formal Verification (2013)

#62

Post by munin »

CHY872 wrote: post #52
ryanobjc wrote: post #18

Earlier quoted context omitted.

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

> if a program compiles one can know that it will never crash

that is not true, you need much stronger guarantees than just typechecking gives you. you also have a large wodge of native code for the runtime that is not written in the strongly typed language.

Re: The Case for Formal Verification (2013)

#63

Post by EzraVinh »

solomatov wrote: post #58
gsnedders wrote: post #57

Earlier quoted context omitted.

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.ke…

But Haskell is also based on some type system, and yet Learn You a Haskell teaches Haskell without formally teaching this type system.

I've been learning Idris and reading the HoTT book at the same time. I'm not sure what it would have been like learning Idris without any formal type theory, but I believe it would be possible.

Re: The Case for Formal Verification (2013)

#64

Post by solomatov »

EzraVinh wrote: post #63
solomatov wrote: post #58

Earlier quoted context omitted.

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.ke…

But Haskell is also based on some type system, and yet Learn You a Haskell teaches Haskell without formally teaching this type system. I've been learning Idris and reading the HoTT book at the same time. I'm not sure what it would have been like learning Idris without any formal type theory, but I believe it would be possible.

The difference here is that type system in case of agda and coq is the core of the language, it's very similar to what operational semantics does with usual programming languages. The type systems is a logic via Curry-Howard correspondence, with which program correctness is proved. In case of Haskell it's just a software engineering tool which helps you find errors in your program in a semi-automatic way.

Re: The Case for Formal Verification (2013)

#65

Post by tluyben2 »

jnbiche wrote: post #36
tluyben2 wrote: post #12

Earlier quoted context omitted.

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

My background is theoretical CS (2 of my professors were pupils of Dijkstra and they were quite particular about formal verification as you can imagine) so that helps; it's good for anyone with an interest in this to read books like 'A discipline of programming' by Dijkstra or more modern books about it (and if you really like it, continue on to Pierce who is the types guy and when I read his some of his work the first time I kind of wondered wth we were doing in programming while this guy already figured it out to such an extent ;).

It all starts to make more sense after some of the theoretical basis. I guess; I don't know how much years of writing formal proofs on pen & paper 20 years ago influenced me in reading this stuff.

Re: The Case for Formal Verification (2013)

#66

Post by ma2rten »

sanxiyn wrote: post #60
ryanobjc wrote: post #21

Earlier quoted context omitted.

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".

Could you elaborate on that? I looked at the article and look at a description of Alloy, it doesn't seem to me like a good example to use for Alloy.

Re: The Case for Formal Verification (2013)

#67

Post by Confusion »

Formal verification and testing are not mutually exclusive and should ideally both be used. If you read this article and conclude that formal verification is the way to go and writing tests is unnecessary, then you are failing to appreciate the concessions Metzger makes. Take e.g.

  but Quark's formal verification doesn't try to show that
  the entire Web browser is correct, and doesn't need to --
  it shows that some insecure behaviors are simply
  impossible. *Those* are much simpler to describe.
Let's assume this is true: we can write interesting programs of relevant size and complexity and prove they are secure. Then we still need a whole bunch of tests to show the program actually does what its users want it to do, because formally specifying that behavior is hard.

Re: The Case for Formal Verification (2013)

#68

Post by lmm »

wsxcde wrote: post #61
rossjudson wrote: post #29

Earlier quoted context omitted.

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".

Model checking deals with two kinds of properties - safety and liveness. Safety properties effectively say nothing bad ever happens while liveness properties say that something good will eventually happen. For example, "my program will never crash due to a null point dereference" is a safety property. "My arbiter module will output a grant for every input request" is a liveness property. It is true that model checker…

> you are inherently limited in terms of what you can prove to whatever it is that the type system can express

Does that actually limit you? E.g. I can imagine using a monad-like structure in Haskell to construct things like "procedure guaranteed to terminate in <k primitive steps".

Re: The Case for Formal Verification (2013)

#69

Post by lmm »

dkarapetyan wrote: post #43
stormbrew wrote: post #40

Earlier quoted context omitted.

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

Suppose I tell you 3 + 2 = 5 and 2 + 3 = 5. Did you learn anything non-trivial about + from those two examples? Did you learn that x + y = y + x for all x and y or that x + (y + z) = (x + y) + z? You can sample as many points as you want and you'll still be no wiser as to how + behaves and how it interacts with * or that the implementation of + even respects any of those properties. If you're going to put in the effo…

> Suppose I tell you 3 + 2 = 5 and 2 + 3 = 5. Did you learn anything non-trivial about + from those two examples? Did you learn that x + y = y + x for all x and y or that x + (y + z) = (x + y) + z?

I gained some evidence. Do you refuse to accept the theory of gravity because we've only measured some examples where F Gm_1m_2 / r^2, not proven it from first principles?

Re: The Case for Formal Verification (2013)

#70

Post by sanxiyn »

munin wrote: post #62
CHY872 wrote: post #52

Earlier quoted context omitted.

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

> if a program compiles one can know that it will never crash that is not true, you need much stronger guarantees than just typechecking gives you. you also have a large wodge of native code for the runtime that is not written in the strongly typed language.

Does Safe Haskell guatantee enough, or do we need more?
Post reply on HN