I like that things like this exist even if I recognize that they are not for me. For some class of system I am sure these languages will shine. It reminds me of Julia - every time I come across it I love the idea of it but I have no personal use for it. I'm always interested in reading articles on dependent type languages like Coq and Idris but I haven't even tried to write a "Hello, World!" in them.<p>I may just be jaded with promises of sufficiently smart compilers. I actually hold out more hope for AI code assistance than I do for easy-to-use formal verification.<p>It is a bit like Esperanto or something like that. Maybe I am just brain damaged from growing up in a world with English and other messy spoken languages but my intuition suggests that perfectly structured languages are possibly the wrong approach.<p>Even though at the time I wanted xhtml to win the battle of structured formats for the web, in hindsight I now believe messy html 5 was the way to go.<p>> We still get buffer overflows and integer overflows. The compiler still cannot tell when our loops will terminate (yes, this is possible). Aliasing is still a complete unbridled mess.<p>As strange as it sounds, I've learned to love the flaws. I don't see my job in life is to remove every possible source of error. There seems to be a balance point where the cure is worse than the disease and I wish to find that balance point rather than some theoretical perfect.<p>So I do hate those things listed. But so far, the balance point for me is with languages that sacrifice perfectly solving those problems.
I've not had as much time to look into formal verification as I'd like and this blew me away<p><pre><code> lemma LemmaFromToBytes(v: nat)
ensures FromBytes(ToBytes(v)) == v {
// Dafny does all the work!
}
</code></pre>
The compiler can _prove_ one function is the inverse of another? That's so cool.<p>Also I disagree with some of the other posts dismissing the usefulness of this kind of thing. I grant that formally verifying every little piece of my code would be overkill. However, I absolutely want certain core pieces of my application formally verified.<p>I'm gonna have to play with Dafny at some point.
SAT solvers are fun. Math is fun. Neither is the most important part of development.<p>Most of my time is not spent formally testing these methods; it is understanding how systems interact and their performance characteristics.<p>I disagree with OP's assertion about legacy languages; they have largely focused their improvements on the areas that actually matter to my day to day development.
The post missed something very important! The whole time I was reading I was thinking to myself “good luck keeping your code error-free after you’re done transcoding from Dafny to the language you actually use in-prod” but…<p>The language (Dafny): <a href="https://github.com/dafny-lang/dafny">https://github.com/dafny-lang/dafny</a><p><i>Dafny is a verification-ready programming language. As you type in your program, Dafny's verifier constantly looks over your shoulder, flags any errors, shows you counterexamples, and congratulates you when your code matches your specifications. When you're done, Dafny can compile your code to C#, Go, Python, Java, or JavaScript (more to come!), so it can integrate with your existing workflow.</i>
The problem with Dafny and other SMT solvers is that when they work, they're brilliant, but when they don't, they're infuriating.<p>Sometimes your code and theorems are formed in a way which Dafny is very good at reasoning about (e.g. standard induction). Then it's nice to just write code and have everything verify.<p>Other times your assertions are non-trivial to the verifier, even if they look obvious, and you must write lemmas and assertions to get them to be proven. And the problem with SMT solvers is that it can be hard to figure out which lemmas and assertions you need to add. It's frustrating to see some assertion Dafny can't prove, which to you seems almost self-evident, and it can be hard to see what is missing.<p>Languages like Coq, Lean, and Isabelle/HOL are better in that you prove things manually (unless you abuse `auto` and tactics for non-trivial proofs, then you still run into the above). Because when you're writing a manual proof, you know exactly what you have and what you need to prove and why the two aren't yet the same. It can still be frustrating but less so, because in Coq you usually have a better idea what key details are unproven, whereas in Dafny you just get "this (entire statement) can't be proved". You could also say that Coq goes "above and beyond" even though you must write the proofs manually, because you can statically check arbitrary properties and write "safe" code which upholds extremely complex invariants using dependent types.<p>But ultimately, <i>any</i> formal verification language becomes extremely verbose and challenging to write once the properties you are trying to statically prove become mildly complicated. Which is why most code doesn't go "above and beyond" even though formal methods have been around for decades. It's an unfortunate reality in the field: you can spend decades writing a formally-verified version of a medium-sized program, or could spend weeks writing the program itself and then writing solid tests (see: CompCert, sel4). But I still think we're making progress: case in point Rust (and other new languages with ownership semantics), and companies actually using formal methods to verify the small but critical parts of your code.
"Dafny’s ability to statically check critical properties of your program goes well beyond what mainstream languages can do (that includes you, Rust)."<p>Ada supports Design by Contract preconditions, postconditions, and type invariants that were pioneered by the Eiffel programming language:<p><a href="https://learn.adacore.com/courses/intro-to-ada/chapters/contracts.html" rel="nofollow noreferrer">https://learn.adacore.com/courses/intro-to-ada/chapters/cont...</a><p>The SPARK subset of Ada also does static proofs / formal verification:<p><a href="https://learn.adacore.com/courses/intro-to-spark/chapters/01_Overview.html" rel="nofollow noreferrer">https://learn.adacore.com/courses/intro-to-spark/chapters/01...</a><p>===<p>Rust has Design by Contract capabilities via the contracts crate:<p><a href="https://docs.rs/contracts/latest/contracts/" rel="nofollow noreferrer">https://docs.rs/contracts/latest/contracts/</a><p>Maybe one day Rust will have formal verification too?<p>Work is under way: <a href="https://alastairreid.github.io/automatic-rust-verification-tools-2021/" rel="nofollow noreferrer">https://alastairreid.github.io/automatic-rust-verification-t...</a>
> The compiler still cannot tell when our loops will terminate (yes, this is possible).<p>Isn't this just the halting problem? Sure, for simple cases compiler could do it (in Java I guess my IDE will do it since the compiler doesn't care), but in the general case, how would a compiler figure this out?
Dafny is a cool language.<p>Conal Eliot, in his 2023 Zurihac talk, says that in order to get efficiency (faster computers that can do more with less) at scale (not merely resilience which we get by adding redundancy and operational tooling) we need languages and tools that allow us to precisely specify the correct program.<p>Dafny is a good step in that direction. I’m also keen to see where the depedently typed programming languages like Lean 4 and Idris 2 will take us. Proof-carrying code could be very useful.
I have tried Dafny. I was quite impressed with how easy it was to set up and the integration with VSCode (even though it was fairly buggy).<p>However it was very difficult to prove things. I often ran into cases where could prove something for 3 byte values, but not 4 bytes, and when I asked about it the answer depended on some really really hardcore internal knowledge of how it worked. E.g. when exactly functions are inlined.<p>So I love the idea, but in practice it seems like it is currently only really usable by people who know how it works internally.<p>That isn't the case with the hardware formal verification tools I've used (e.g. VC Formal) which I have very little clue how they work (it's basically magic as far as anyone I've asked is concerned) but I can use them very easily.<p>I suspect formally verifying hardware is easier than software but there you go.
I'm a believer too (in dependent types). Software already bears an ungodly amount of responsibility, and with AI it will only become more so. Correctness is critical. While tests are good, it's impossible yo cover every case. Compiler-verifiable properties are better.
This is pretty cool!<p>I do have a nitpick I think is important. An empty byte array getting converted to zero seems like a bad edge case that should probably produce some kind of error invariant.<p>This isn't a minor concern if the intent is to use this in serious applications that require this degree of formalism. The two proofs are easy to break: `ToBytes(FromBytes([])) != []`. It's an obvious example of the issue: FromBytes handles inputs ToBytes can't generate therefore they are not true inverses of each other.<p>It's a simple case but it was quick to find in this simple example, and it hints at dangerous oversights that could lead to severe bugs in more complex scenarios, like in cryptography. It's critical to account for such edge cases.
Amazon uses Dafny to ensure that their authorization engine makes correct decisions: <a href="https://www.amazon.science/blog/how-we-built-cedar-with-automated-reasoning-and-differential-testing" rel="nofollow noreferrer">https://www.amazon.science/blog/how-we-built-cedar-with-auto...</a>
Formal verification is very cool and definitely has its uses (<a href="https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf" rel="nofollow noreferrer">https://www.sigops.org/s/conferences/sosp/2009/papers/klein-...</a>). From what I heard at least some chip manufacturers do formal verification of their chip designs.<p>But I don't think it scales to general-purpose programming. Most of the easy-to-verify conditions could (and should) be checked by asserts and unit tests. But there's a whole layer of complexity on top of that and in my experience it accounts for the bigger share of bugs.
An introductory course to the use of Dafny for writing programs with fully verified specifications may be found at [1].<p>[1] <a href="https://www.doc.ic.ac.uk/~scd/Dafny_Material/Lectures.pdf" rel="nofollow noreferrer">https://www.doc.ic.ac.uk/~scd/Dafny_Material/Lectures.pdf</a>
Interestingly the postcondition does not prove that the GCD implementation is correct and by extension does not prove Bézout's identity.<p>Stating that some value is the gcd is surprisingly tricky. Once you have proven that Bézout's identity holds for your function you could prove it is the actual gcd by showing it is a divisor for both a an b. Assuming I understood the notation correctly that would give something like the following<p><pre><code> lemma euclid_gcd(nat: a, nat: b)
ensures (a % GCD(a,b)) == 0
ensures (b % GCD(a,b)) == 0
{ }
</code></pre>
I'd be curious to know if it can prove this. Note that this would still not constitute a proof of Bézout's identity, as it uses it to define what the gcd is. Thankfully defining the gcd using Bézout's identity is pretty common nowadays, as it allows for a useful generalisation of the concept.
>function Gcd(a:nat, b:nat) : (g:nat,x:int,y:int))<p>I hope this is a typo. Otherwise it…requires an unmatched close paren?<p>That's a new level of cursed syntax.<p>EDIT: Also, is |array| a common way to get the length of an array in languages? I've never seen that (or some of this other syntax) before and it took me a minute to figure out what was happening.
Shout out to F#. I think it does a lot of this, doesn't get much respect I think because it is from MS and runs on .NET.<p>Love the type checking, which I think is better than Rusts. But since I think Rust will win the market, I hope it improves.
well this is a surprise, He was my old lecture (one of the best at my university tbh). Was always obsessed with formal verification. I remember him trying make us use a formal verification programming language he created called whiley, Which was a java based language and was pretty terrible and filled with bugs lol but had some cool ideas in it
Hope people are not going to mention that this is a blockchain company. No matter how I don't like it; this work, research and others (like Wadler) is great and very interesting advancements in the software verification space. You can ignore the blockchain side of things.
This is indeed an interesting approach, but I wonder whether it also allows you to define 'implementations'. Let me explain.<p>A lot of software development done is because computers are too slow for our demand.[1] It is nice to have an integer type 'nat' that can hold arbitrary large integer numbers (at least as large as fits in the memory model, I presume), but it is not very efficient to use it for every purpose. You also would like to have methods to verify that a certain implementation of a program using a certain 'limited' representation of integers, is correct.<p>[1] <a href="https://www.iwriteiam.nl/AoP.html" rel="nofollow noreferrer">https://www.iwriteiam.nl/AoP.html</a>
Static typing in programming languages are propositions[1] that the type checker proves (because it is a prover of sorts). It's very simple; it has to be simple to ensure that it's reasonably fast and above all, terminates with a clear yes/no.<p>It's a bit off for this article not to mention that whatever cleverness underlies these examples, things will fail. That is it may not terminate in general, and if it does it might well do so without proving anything useful. I really, really like the idea of formal methods and I would really, really love to use them but they don't come for free unfortunately.<p>[1] in an informal sense, perhaps calling them proposals might be better
Could anyone comment on how often Dafny finds proofs for useful theorems on its own in practice, without requiring the programmer to use expert knowledge of the proof search system to break it down into a sequence of gettable lemmas and/or refactor the code?<p>If the answer is "not that often", is there a possibility that LLM integration could help with proof search? This seems like an application where getting it 95% right is actually OK since proofs generated by the LLM can be automatically checked for correctness.
<p><pre><code> lemma LemmaFromToBytes(v: nat)
ensures FromBytes(ToBytes(v)) == v {
// Dafny does all the work!
}
</code></pre>
> This might not seem like much, but it represents something you cannot easily do in other languages. This lemma asks Dafny to check that, for any possible nat value v, it always holds that FromBytes(ToBytes(v)) == v. Again, Dafny checks this at compile time — no testing required!<p>---<p>How long does it take, do we rely on caching compilation results here? Is it iterating through all values?
Cool article. This language looks really interesting. The only problem though is, how do I use it? The majority of the programming I do in my daily life revolves around performing actions in a database based upon the contents of HTTP requests. There's lots of amazing programming languages out there, however there don't seem to be any really pushing the boundaries for web programming.
Theorem proving is a interesting area of Computer Science. I personally like using ACL2, which has proven itself through industrial use: <<a href="https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5597723/" rel="nofollow noreferrer">https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5597723/</a>>.
If Dafny is not production ready, what language can I use with similar formal verification features and that is already used in production in mission critical environments?
I have a very bad opinion about this, why there were no quantum leaps in programming: in practical world there is just no time to think out of the box. its an endless crunch and race to ship, so something brand new and „risky“ can only be born out of strong vision and necessity.
On the other hand if we take PL research - it is too far detached from practical reality. Have you ever tried grokking type proofs? It is driven by a separate breed of mathematicians that cosplay as programmers and they build their „perfect and sound“ (and useless) world. Do you know how many tons of (garbage) papers were in the era when AOP was the rage? What are the practical results? And where are they? Or take Haskell as an emple, where nobody can clearly explain to a java codemonkey what a goddamn monad is? Or endless continuations and effects research and formalisms by Felleisen and Kiselyov only for all of it be kinda rediscovered and slapped on by react devs? Useless, all of it.