6 ms·

Dafny: Verification-Aware Programming Language

64 points by MindGods 6y ago

dwohnitmok 6y ago
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 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!
- mcguire 6y ago
  Dafny (and formal verification for imperative languages) is a lot of fun. But does Dafny have any library documentation? Is it .Net?
  - dwohnitmok 6y 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.
    - mcguire 6y ago
      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.
pubby 6y 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 6y 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
- dwohnitmok 6y 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/ 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.
- MaxBarraclough 6y 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-management-in-ada-and-spark https://www.adacore.com/papers/safe-dynamic-memory-managemen... [1] https://arxiv.org/abs/1805.05576 https://arxiv.org/abs/1805.05576
  - 1tCKV3QfIo 6y ago
MaxBarraclough 6y 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/basic.html http://docs.adacore.com/spark2014-docs/html/ug/en/source/bas... * https://github.com/tofgarion/spark-by-example https://github.com/tofgarion/spark-by-example
- dwohnitmok 6y 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 https://rise4fun.com/Dafny/tutorial that has the standard mathematical definition of Fibonacci numbers as a function and then implements it as a method).
  - MaxBarraclough 6y 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/ https://stackoverflow.com/a/57169728/
replwoacause 6y ago
But what is that logo? Yikes...
manu3000 6y ago
also similar is why3 http://why3.lri.fr/ http://why3.lri.fr/
norswap 6y ago
In the same vein: http://whiley.org/about/overview/ http://whiley.org/about/overview/
lambdatronics 6y 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).

64 points by MindGods 6y ago

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 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!

mcguire 6y ago
Dafny (and formal verification for imperative languages) is a lot of fun. But does Dafny have any library documentation? Is it .Net?
- dwohnitmok 6y 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.
  - mcguire 6y ago
    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.

pubby 6y 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 6y 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

dwohnitmok 6y 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/ 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.
MaxBarraclough 6y 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-management-in-ada-and-spark https://www.adacore.com/papers/safe-dynamic-memory-managemen... [1] https://arxiv.org/abs/1805.05576 https://arxiv.org/abs/1805.05576
- 1tCKV3QfIo 6y ago

MaxBarraclough 6y 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/basic.html http://docs.adacore.com/spark2014-docs/html/ug/en/source/bas... * https://github.com/tofgarion/spark-by-example https://github.com/tofgarion/spark-by-example

dwohnitmok 6y 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 https://rise4fun.com/Dafny/tutorial that has the standard mathematical definition of Fibonacci numbers as a function and then implements it as a method).
- MaxBarraclough 6y 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/ https://stackoverflow.com/a/57169728/

replwoacause 6y ago

But what is that logo? Yikes...

manu3000 6y ago

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

norswap 6y ago

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

lambdatronics 6y 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).