Dafny: Verification-Aware Programming Language | Hacker News Reader

Dafny: Verification-Aware Programming Language

github.com

64 pointsMindGods26 comments

I found a good summary on StackOverflow:

"Dafny is based on a Java or C# like imperative language with the ability to write Hoare logic style state invariants, this allows users of the languages to verify properties about methods, and objects that use mutable state, loops, arrays, and so on. Dafny's core theory is a custom program logic mostly designed by Rustan and a handful of collaborators. Dafny discharges the verification conditions it generates by compiling them to Boogie an intermediate verification language, which in turn compiles them into queries which are passed to an SMT solver such as Z3 or CVC4 to discharge." - jroesch

If you don't want to install anything, you can get a taste of Dafny by looking at its online tutorial.

https://rise4fun.com/Dafny/tutorial

Dafny is a good example of what formal verification looks like for imperative languages (as opposed to e.g. dependent types for functional languages). Gotta love loop invariants!

Dafny (and formal verification for imperative languages) is a lot of fun.

But does Dafny have any library documentation? Is it .Net?

I'm not quite sure what you mean.

Dafny compiles to .NET indeed. What do you mean by library documentation? Dafny doesn't have many (any? I certainly haven't used any...) libraries to begin with.

I thought Dafny has access to the .NET infrastructure. But when I played with Dafny a while back, the only library interface I saw was printing to stdout (IIRC), which would imply that Dafny was a toy language intended for playing with verification and not much else. On the other hand, I've heard otherwise---it's been used for Windows drivers?---but without any documentation or examples, I lost interest.

Good stuff. Can anyone comment on how it compares against SPARK Ada?

At a glance it looks like Dafny has functional programming features, and looks quite approachable. Its compiler targets .Net, unsuitable for critical-systems work. Are there plans for it to get an industry-strength compiler, or is the emphasis on research rather than critical-systems software development?

SPARK examples for the curious:

* http://docs.adacore.com/spark2014-docs/html/ug/en/source/bas...

* https://github.com/tofgarion/spark-by-example

I've only ever watched SPARK Ada from afar and never written code using it, so keep in mind that my comment might be a bit one-sided.

I doubt Dafny will have native targets (which I assume is a prerequisite for the "critical-systems" work you're talking about) any time soon if ever. There's just not enough resources behind it. AFAICT, basically all the development, Stack Overflow answering, etc. is all powered by a single dude (Rustan Leino). So I don't think it'll be competing in the same space as SPARK Ada any time soon simply due to resource availability.

Nonetheless Dafny as a language is, I think, strictly more expressive than SPARK. For example, Dafny's functions (vs methods) allow for the very nice expression of arithmetic invariants that I don't think SPARK supports (look at the Fibonacci example in the online tutorial here: https://rise4fun.com/Dafny/tutorial that has the standard mathematical definition of Fibonacci numbers as a function and then implements it as a method).

> I doubt Dafny will have native targets (which I assume is a prerequisite for the "critical-systems" work you're talking about) any time soon if ever

Fair enough. Still a really neat project.

I forgot to ask an obvious question: Dafny uses .Net's garbage collection, right? If so, that presumably rules out its use on hard real-time systems.

> the Fibonacci example in the online tutorial

For anyone struggling to find it, ctrl-f for completed Fibonacci

I agree the Dafny syntax is very tidy.

Surprisingly I wasn't able to find a directly comparable SPARK program. The closest I could manage was populating an array with the Fib sequence, by someone on StackOverflow (I haven't verified it) [0]

[0] https://stackoverflow.com/a/57169728/

Perhaps worth noting is Armada

https://github.com/microsoft/Armada

which is built upon Dafny and targets a C-like language.

Thanks, I hadn't heard of that project. Their paper is at [0] (which I've only skimmed terribly quickly). I'm not quite sure what to make of 'targets a C-like language'. Does that mean, put bluntly, that it's not practical? Can it be made to target standard C?

While we're here, a shoutout to ZZ / ZetZ, [1] which we discussed 5 months ago at [2]. It's a verifiable C-style language which compiles down to standard C. I'm not sure how mature the language is at this point. (It still pains me that my prominent comment at [2] turned out to be fundamentally mistaken.)

And let's finish up the tour with a quick mention of Frama-C [3] and the (sadly proprietary) Escher C Verifier, [4] both of which work with C directly.

[0] https://jamesrwilcox.com/armada.pdf

[1] https://github.com/zetzit/zz

[2] https://news.ycombinator.com/item?id=22245409

[3] http://frama-c.com/acsl_tutorial_index.html

[4] https://www.eschertech.com/products/ecv.php

From the paper you can see that they actually target CompCertTSO (a C subset)

https://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/

from the CompCert folks - who do formally verified C compilers (also worth looking at, btw). Targeting a subset of C allows them to preserve their behavioral guarantees in way that would be challenging I think with the full C language. So it's not an unreasonable subset to pick if you're serious about predictable outcomes.

Thanks. I read Via a C-like language to mean their language compiles to a non-standard language resembling C, but as you say, they mean they defined a novel language that resembles C, and it compiles down to standard C (specifically, the C subset named ClightTSO suitable for use with the CompCertTSO compiler).

Nowhere in Armada's overview [0] is it stated that the ultimate goal is to produce verified C code.

I've heard of CompCert. Pity it hasn't got more traction. Also a pity about its licensing situation. The Free and Open Source community is not interested in semi-Free software. The DMD compiler showed us this.

[0] https://github.com/microsoft/Armada

Update: I created a GitHub Issue to point out the omission. The overview has now been clarified.

"I forgot to ask an obvious question: Dafny uses .Net's garbage collection, right? If so, that presumably rules out its use on hard real-time systems."

I was just about to point that out. Yes, Dafny uses garbage collection (which makes formal verification much easier). As far as I know in SPARK (and FRAMA-C), verification of memory allocation is still an open research question.

Sure it does have native targets. It can compile to C++, Go, JS, and many more. And you forgot that Dafny has Microsoft behind, so I would rate it ahead of Spark ADA. Visual Studio support.

It also has a much nicer syntax, also compared to ATS, which is in the same league.

But are those backends complete? I.e. do they support all of Dafny? Last I programmed in Dafny I don't think any alternative back end did.

Also Dafny has pretty poor IDE support. I don't think it has Visual Studio support and the plugin for Visual Studio Code is not written by MS (and is pretty bare bones).

MS really only supports Dafny by employing its creator. It doesn't seem to devote any other resources.

Again I haven't programmed with SPARK before but my impression is that it's getting way more industry use and support.

> Again I haven't programmed with SPARK before but my impression is that it's getting way more industry use and support.

Correct, it's been used in numerous life-or-death systems. Perhaps most famously, the software of the Boeing 777 is almost entirely SPARK based. [0][1] Dafny has not, it seems to be more of a research project.

> MS really only supports Dafny by employing its creator. It doesn't seem to devote any other resources.

Right. It would be interesting if Microsoft decided to compete in the critical-systems space, but I doubt they will. With SPARK Ada, all the real work seems to happen at AdaCore. [2] There are various different high-assurance Ada compilers available though.

[0] https://www.cse.msu.edu/~cse814/Lectures/09_spark_intro.pdf

[1] https://www.ei.tum.de/fileadmin/tueifei/rcs/becker/spark2014...

[2] https://www.adacore.com/

This .... This kind of approach could and should replace rust. That is, if the language developers are interested in commercial adoption a sweet spot is a memory safer c++. Rust has that going on but it'll never make it as a truly safe language in memory and other aspects without specification and verification. I'm arguing real progress may include rust like impulses but can't be complete without built in tla+ or other formal tool support

TLA+ operates at a different level both conceptually and in the SDLC than programming languages like Dafny or Rust. TLA+ is a design language rather than an implementation language and this permeates a lot of its foundations.

FWIW you can already use Dafny to write individual modules in real-world programs (it compiles to .NET and therefore interoperates with e.g. C#), although there are still some rough edges given the tiny size of its community, and the documentation for doing this is rather fragmentary.

As for the difference between Dafny and Rust, Rust really has only one big unique trick up its sleeve which is its affine types. Otherwise its approach is entirely compatible with Dafny's (and indeed there are efforts to port over some the same ideas between Dafny to Rust, see e.g. https://alastairreid.github.io/rust-verification-tools/). Those will take a long time though to come to fruition because formal verification is still a hard problem.

It wasn't a mistake for Rust not to emphasise formal verification. Going that route would have been very restrictive. Rust is aiming to offer a safer alternative to C, not a more approachable formally verifiable language.

That said, it looks like the good ideas from Rust may find their way into SPARK, a highly restrictive programming language for critical systems development with formal verification. [0][1]

[0] https://www.adacore.com/papers/safe-dynamic-memory-managemen...

[1] https://arxiv.org/abs/1805.05576

> This kind of approach could and should replace rust.

Rust could definitely be augmented with formal verification; it's just that this requires more research into semantics for Rust itself and Rust-like languages - especially wrt. the 'unsafe' subset.

If you're interested in a C/Rust-level language which supports verification, maybe take a look at ATS http://www.ats-lang.org

This is really cool! Having verification and Hoare logic as first-class language features seems like a better approach than trying to verify a language that wasn't built to be verified (like what sel4 is doing with C).

In the same vein: http://whiley.org/about/overview/

also similar is why3 http://why3.lri.fr/

But what is that logo? Yikes...

Reply on news.ycombinator.com