This formal verification course I took by Manos Kapritsos and Jon Howell is taught in Dafny and assumes no former experience with the subject. Most of the exercises are to some degree “self-grading” as proof success means you have a correct solution, provided your spec is correct. I highly recommend.
I quite like Dafny, despite my first run up with it (verification aspect) being frustrating. The language is well designed for this. Also, it looks like it is a great candidate as a code generation target for LLMs because you can generate the proof of correctness and run a feedback loop with Dafny's checker.
Try writing a^b in integers and proving its correctness. The simple version works (based on a x a^(b-1)). But if you write an "optimised one" using (with handwaved details) (a^(b/2))^2 .... pulled some serious hair trying to prove this function works.
Not a stupid question at all. There are two reasons verification tends to happen in these specialized languages: the languages we usually use are often not expressive enough to write things like specifications, and a bit too expressive in the sense of letting people write program logic that is insanely difficult to verify (think untyped pointers into a dynamically allocated heap for example). So these verification related languages often are more expressive on the spec side and more restrictive in terms of what kind of code you can write.
Yes, but the quality of the spec varies. For example many (most?) C programs have undefined behaviors which means the spec is incomplete and unreliable. Dafny gives you better tools to avoid this. So in the end you get a higher quality spec with Dafny.
> … verify/synthesize invariants in languages people use?
Good question. This is the holy grail. This is what everyone in PL research would love. This is where we want to get to.
Turns out a language as “simple” as C has sufficiently complicated semantics as to limit rigorous analysis to the basics. One example is loop analysis: it’s very useful to know that a loop will terminate eventually; if a loop is modifying some state and—worse—if the iteration variable gets modified—kiss your analysis goodbye because mechanically synthesizing strong pre- and post-conditions becomes insurmountable. It’s not an engineering challenge. It’s a math/pure CS theory challenge.
Right. The problem is that those languages are relatively permissive in their type systems. Obviously Rust can capture more in its type system than C can. You would probably want a type like “decreasing unsigned integer” for Rust and some way to enforce monotonic decreasing, which Rust doesn’t give you.
(Any experts on formal verification please correct any inaccuracies in what I say here.)
The upshot of it is that C, C++, and Rust permit too much behavior that isn’t capturable in the type system. Thus, the properties that you’re interested in are semantic (as opposed to syntactic; type systems turn semantic properties into syntactic ones) so Rice’s theorem applies and there’s no computable way to do the analysis right.
Most existing mainstream languages aren’t expressive enough to encode these invariants. For languages outside of the mainstream, Lean 4 is a language supporting verification, and it’s also a full programming language, so you can write your proofs/theorems in the same language that you program in.
In most languages you can express any invariant, sure, but you can't prove that the invariant is upheld unless you run the program.
For example a NonNegativeInteger type in most languages would just have a constructor that raises an exception if provided with a negative number. But in languages with proofs, the compiler can prevent you from constructing values of this type at all unless you have a corresponding proof that the value can't be negative (for example, the value is a result of squaring a real number).
That's what we use when we can limit our loop count and recursion depth somehow. Prove it for small data, and infer from it for big data.
I use C and C++ model checkers, like cbmc and its variants (esbmc) successfully, but you need to adjust your tests and loops a bit.
Like #ifdef __VERIFIER__ or #ifdef __CPROVER__
https://diffblue.github.io/cbmc/cprover-manual/index.html
Dafny and similar languages use SMT; their semantics need to be such that you're giving enough information for your proof to verify in sufficient time, otherwise you'll be waiting for a very long time or your proof is basically undecidable.
I'm not sure about benchmarks comparing languages, but Dafny goes through a lot of tweaking to make the process faster.
Dafny has been around for a while and people do in fact use it. People also apply contract languages to C and all matter of other things, so really question boils down to "Why arent you doing what I expect of you?"
I got a bit into SPARK (a subset Ada of that has formal verification) with AoC, and while it can be tricky, SPARK is quite flexible in how much you prove. Dafny sounds interesting, but I can't find a comparison between the two. There's obviously a difference in memory management, but the rest looks quite similar at first sight, and their niche is quite similar. Does anyone know of a (deeper) comparison between both languages?
One difference is that SPARK is intended primarily for safety critical, real-time software (often for embedded systems), while Dafny is meant for teaching purposes and non-real time applications (i.e. environments where a large runtime and garbage collection are permissible). Dafny compiles to C#/Java/Go/etc. and is meant to be interoperable with them so I think it aims at similar use cases as those languages.
Dafny is quite different from Scala in that it is a formal language that can be compiled to a number of different targets such as Go or Python or C#. This allows an algorithm to be formally verified while still producing executable code.
You could add Scala as a compilation target or you could just use the Java output and call formally verified Java functions from Scala. Even if you do get an implementation that produces Scala, don't expect the full power of idiomatic Scala to be available in the code you formally verify. To verify code, you have to write the code in Dafny with associated assertions to be proven. Since there are multiple compilation targets multiple formal constraints on what can usefully be verified, the data types available will not match the data types that you would use natively from Scala.
It's similar in spirit, but in Dafny one can express much more complicated and complex invariants which get checked at build time -- compared to eiffel where pre/post conditions are checked at runtime (in dev builds mostly).
Interestingly, though, you can have some runtime checking with Dafny as well as the formidable dependent type checking and formal verification that happens at build time.
That means that most of the proof can be done ahead of time with just some loose ends verified using an SMT prover at runtime.
Yes, the primary reason being the bootstrapping problem. But because Dafny can already can generate C# code, that should not be a major problem. It also allows for a gradual conversion where more and more parts are generated from Dagny sources.
I know that maintaining a compiler in its own language poses some problems when you want to extend that language with additional features.
Because compilers are rather complex problems, they can be viewed as a testing stone for a language.
I think it would be nice to have a formally verified compiler. That is a bit more than proving that the sources are correct. But because formally verified compilers are rare, it could promote the usages of Dayne.
I am aware that it would be quite an effort to make it self-hosted and even more to formally verify it correctness.
This formal verification course I took by Manos Kapritsos and Jon Howell is taught in Dafny and assumes no former experience with the subject. Most of the exercises are to some degree “self-grading” as proof success means you have a correct solution, provided your spec is correct. I highly recommend.
https://glados-michigan.github.io/verification-class/fall202...
I quite like Dafny, despite my first run up with it (verification aspect) being frustrating. The language is well designed for this. Also, it looks like it is a great candidate as a code generation target for LLMs because you can generate the proof of correctness and run a feedback loop with Dafny's checker.
Try writing a^b in integers and proving its correctness. The simple version works (based on a x a^(b-1)). But if you write an "optimised one" using (with handwaved details) (a^(b/2))^2 .... pulled some serious hair trying to prove this function works.
Am working on rewriting an imperative programming course to use Dafny to present verified algorithms and data structures.
Please post HN when you finish.
This might be a stupid question, but why a separate programming language rather than aiming to verify/synthesize invariants in languages people use?
Not a stupid question at all. There are two reasons verification tends to happen in these specialized languages: the languages we usually use are often not expressive enough to write things like specifications, and a bit too expressive in the sense of letting people write program logic that is insanely difficult to verify (think untyped pointers into a dynamically allocated heap for example). So these verification related languages often are more expressive on the spec side and more restrictive in terms of what kind of code you can write.
Yeah I can see pointer weirdness being an issue.
As for being not expressive enough for specifications, isn't the code itself a form of specification? :)
Yes, but the quality of the spec varies. For example many (most?) C programs have undefined behaviors which means the spec is incomplete and unreliable. Dafny gives you better tools to avoid this. So in the end you get a higher quality spec with Dafny.
> … verify/synthesize invariants in languages people use?
Good question. This is the holy grail. This is what everyone in PL research would love. This is where we want to get to.
Turns out a language as “simple” as C has sufficiently complicated semantics as to limit rigorous analysis to the basics. One example is loop analysis: it’s very useful to know that a loop will terminate eventually; if a loop is modifying some state and—worse—if the iteration variable gets modified—kiss your analysis goodbye because mechanically synthesizing strong pre- and post-conditions becomes insurmountable. It’s not an engineering challenge. It’s a math/pure CS theory challenge.
Dafny seems to have loops too, and the way it solves the problem you mentioned is forcing the user to write these invariants.
I assume if you were to develop such a system for C, C++, or Rust you'd similarly expect the user to do this.
Right. The problem is that those languages are relatively permissive in their type systems. Obviously Rust can capture more in its type system than C can. You would probably want a type like “decreasing unsigned integer” for Rust and some way to enforce monotonic decreasing, which Rust doesn’t give you.
(Any experts on formal verification please correct any inaccuracies in what I say here.)
The upshot of it is that C, C++, and Rust permit too much behavior that isn’t capturable in the type system. Thus, the properties that you’re interested in are semantic (as opposed to syntactic; type systems turn semantic properties into syntactic ones) so Rice’s theorem applies and there’s no computable way to do the analysis right.
You are answering a question you want to answer, not the one I asked! :)
Yes, dependent types can encode nice constraints, but so can asserts and assumes.
I am not seeing the fundamental difference in yeeting these constraints to a solver. Dafny seems to do the same thing with Z3.
Most existing mainstream languages aren’t expressive enough to encode these invariants. For languages outside of the mainstream, Lean 4 is a language supporting verification, and it’s also a full programming language, so you can write your proofs/theorems in the same language that you program in.
What's an invariant you can not encode in a general purpose programming language?
I'd have assumed, by virtue of being Turing complete, you could express any invariant in almost any language?
In most languages you can express any invariant, sure, but you can't prove that the invariant is upheld unless you run the program.
For example a NonNegativeInteger type in most languages would just have a constructor that raises an exception if provided with a negative number. But in languages with proofs, the compiler can prevent you from constructing values of this type at all unless you have a corresponding proof that the value can't be negative (for example, the value is a result of squaring a real number).
That's what we use when we can limit our loop count and recursion depth somehow. Prove it for small data, and infer from it for big data.
I use C and C++ model checkers, like cbmc and its variants (esbmc) successfully, but you need to adjust your tests and loops a bit. Like #ifdef __VERIFIER__ or #ifdef __CPROVER__ https://diffblue.github.io/cbmc/cprover-manual/index.html
There seems to be a bunch of papers and tools that extend CBMC for unbounded loops with k-induction!
The semantics of Dafny is carefully designed to make verification efficient.
Dafny can compile to and interface with a few languages, including C#.
What does it mean for verification to be efficient?
Are there benchmarks showing dafny is faster than other inefficient options ?
Dafny and similar languages use SMT; their semantics need to be such that you're giving enough information for your proof to verify in sufficient time, otherwise you'll be waiting for a very long time or your proof is basically undecidable.
I'm not sure about benchmarks comparing languages, but Dafny goes through a lot of tweaking to make the process faster.
Dafny has been around for a while and people do in fact use it. People also apply contract languages to C and all matter of other things, so really question boils down to "Why arent you doing what I expect of you?"
I got a bit into SPARK (a subset Ada of that has formal verification) with AoC, and while it can be tricky, SPARK is quite flexible in how much you prove. Dafny sounds interesting, but I can't find a comparison between the two. There's obviously a difference in memory management, but the rest looks quite similar at first sight, and their niche is quite similar. Does anyone know of a (deeper) comparison between both languages?
One difference is that SPARK is intended primarily for safety critical, real-time software (often for embedded systems), while Dafny is meant for teaching purposes and non-real time applications (i.e. environments where a large runtime and garbage collection are permissible). Dafny compiles to C#/Java/Go/etc. and is meant to be interoperable with them so I think it aims at similar use cases as those languages.
Reminds me of Eiffel, in a good way. Looks awesome. Is there anything close to this in Scala by chance?
Dafny is quite different from Scala in that it is a formal language that can be compiled to a number of different targets such as Go or Python or C#. This allows an algorithm to be formally verified while still producing executable code.
You could add Scala as a compilation target or you could just use the Java output and call formally verified Java functions from Scala. Even if you do get an implementation that produces Scala, don't expect the full power of idiomatic Scala to be available in the code you formally verify. To verify code, you have to write the code in Dafny with associated assertions to be proven. Since there are multiple compilation targets multiple formal constraints on what can usefully be verified, the data types available will not match the data types that you would use natively from Scala.
It's similar in spirit, but in Dafny one can express much more complicated and complex invariants which get checked at build time -- compared to eiffel where pre/post conditions are checked at runtime (in dev builds mostly).
Interestingly, though, you can have some runtime checking with Dafny as well as the formidable dependent type checking and formal verification that happens at build time.
That means that most of the proof can be done ahead of time with just some loose ends verified using an SMT prover at runtime.
This expressiveness is a curious point, because a common charge leveled against Scala is that it is too expressive.
Expressiveness tends to become a liability when the benefits of the expressiveness aren’t clear.
Dafny’s expressiveness tends to be more in the service of coherent specifications and less in the service of language abstraction for its own sake.
This looks pretty neat, but the mapping to other languages looks rather awkward for string types (for example).
Fine for teaching, but it doesn't seem to be a suitable tool to generate idiomatic library code?
Looks interesting. I saw some C# files, from which it seems it is implemented in C#. Is there going to be an implementation in Dafny?
It could be done, but what would be the virtue of it? Most programming languages are not self-hoisted for a reason.
Yes, the primary reason being the bootstrapping problem. But because Dafny can already can generate C# code, that should not be a major problem. It also allows for a gradual conversion where more and more parts are generated from Dagny sources.
I know that maintaining a compiler in its own language poses some problems when you want to extend that language with additional features.
Because compilers are rather complex problems, they can be viewed as a testing stone for a language.
I think it would be nice to have a formally verified compiler. That is a bit more than proving that the sources are correct. But because formally verified compilers are rare, it could promote the usages of Dayne.
I am aware that it would be quite an effort to make it self-hosted and even more to formally verify it correctness.