Dafny: A Language and Program Verifier for Functional Correctness | Hacker News Reader

Dafny: A Language and Program Verifier for Functional Correctness

research.microsoft.com

56 pointskushti10 comments

Good to see it show up on HN. It's a nice language and their rise4fun project brings such stuff to a wider audience. I wonder if any readers with a lot of hands-on experience in these can tell me how it compares to SPARK Ada. About the same? Behind in capabilities? Ahead in some ways?

SPARK would seem to be the definitive baseline to compare all the others, too.

Source: http://dafny.codeplex.com/SourceControl/latest

I like it. The Dafny annotations seem straightforward and approachable.

Anyone know of a similar system for Javascript?

Does anyone have an estimate to the difficulty of using Dafny as an annotation to programs written in another programming language? I'm thinking of one on a different OS (Linux) than the MS Windows OS for which Dafny appears to be written.

Eruhm

Is it just me, or is describing the functional correctness of a program with another programming language asking for more problems?

Not to me. I've found unit tests to be indispensable in establishing and maintaining code correctness -- and my unit tests have always been written in a PL, too.

There are two cruical properties you want, I think:

A) It must be possible to automatically and completely mechanically ensure that implementation & proof don't get out of sync. Having a formal proof for an algorithm which isn't the algorithm that you've actually ended up implementing doesn't really help you one whit :). This is relatively simple for unit tests and property-based tests like QuickCheck: Just observe that the number of tests run actually increases over time and never decreases unexpectedly. (Actually, it seems to be rather rare to have support from Continuous Integration tools for tracking the latter.)

B) There must be (in some sense) at least some non-trivial difference between the implementation & "proof". (At the absurd extreme: bisimulation doesn't really work as proof of anything if the implementations are one and the same.) For example, in Idris the implementation is basically just code while the proof is the accomanying types -- which ensures that they're not basically just saying the (trivially) same thing, even though the types greatly constrain what the implementation can do.

I think that the allure of "practical" dependent types (e.g. Idris) may be that such languages trivially obey both properties. Of course you still end up with a "trusted computing base" which is non-trivial in such cases.

Property-based checking [1] is pretty much the paragon of proving the mathematical correctness of a program short of a) using something like SPARK and Ada, or b) using Coq or Agda to formally verify, well, everything[2]. Formal verification is difficult but most of the rigorous proofs are done exclusively outside of the language in which they were written[3].

[1] https://wiki.haskell.org/Introduction_to_QuickCheck2

[2] http://www.slideshare.net/jasonreich/formal-verification-of-...

[3] http://adam.chlipala.net/papers/ImpurePOPL10/ -- The field is moving too fast for me to keep up, but last I checked the theoretical comp. sci. guys were still using a methodology similar to this. I haven't read many POPL or ICFP papers in the last few years so someone who's more in touch with cutting-edge research, please jump in.

It's another thing that can go wrong. That's definitely true. The good news is that they sort of complement each other: errors in one help you spot errors in the other. Plus, picking the right one makes spotting problems visually much easier.

Thing is, almost all the problems in systems have happened due to coding and interface problems. Especially hidden assumptions. Formal verification and static analysis are great at dealing with that. They prevent and catch many more problems than they introduce despite problems occurring in specs or proofs. It's like a combo of a numbers game and applying proven principles.

Hope that makes sense.

It's not significantly different from describing correctness in, say, tests written in the same language. By doing something twice, you would have to make the same mistake for it to sneak through.

The specification is also easier to write because you don't have performance constraints and you're using a different set of abstractions than your main code.

Reply on news.ycombinator.com