Dafny: Verification-Aware Programming Language

by MindGods • 6 years ago

64 26 6 years ago

dwohnitmok5• 6 years ago

If you don't want to install anything, you can get a taste of Dafny by looking at its online 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!

mcguire3• 6 years ago

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

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

dwohnitmok5• 6 years ago

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.

pubby• 6 years ago

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

doonesbury• 6 years ago

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

dwohnitmok5• 6 years ago

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.

MaxBarraclough7• 6 years ago

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

zozbot234• 6 years ago

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.

chriswarbo• 6 years ago

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

MaxBarraclough7• 6 years ago

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

dwohnitmok5• 6 years ago

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

MaxBarraclough7• 6 years ago

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/

rurban• 6 years ago

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.

replwoacause• 6 years ago

But what is that logo? Yikes...

manu3000• 6 years ago

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

norswap• 6 years ago

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

lambdatronics• 6 years ago

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

Dafny: Verification-Aware Programming Language

Related Stories