4 ms·

Dafny: Verification-Aware Programming Language

110 points by handfuloflight 11mo ago

dionian 11mo ago
Reminds me of Eiffel, in a good way. Looks awesome. Is there anything close to this in Scala by chance?
- gz09 11mo ago
  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).
  - ted_dunning 11mo ago
    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.
  - esafak 11mo ago
    This expressiveness is a curious point, because a common charge leveled against Scala is that it is too expressive.
    - steego 11mo ago
      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.
- ted_dunning 11mo ago
  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.
fjfaase 11mo ago
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?
- algorithmsRcool 11mo ago
  It could be done, but what would be the virtue of it? Most programming languages are not self-hoisted for a reason.
  - fjfaase 11mo ago
    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.
- deleted 11mo ago
  [deleted]
fooker 11mo ago
This might be a stupid question, but why a separate programming language rather than aiming to verify/synthesize invariants in languages people use?
- quamserena 11mo ago
  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.
  - fooker 11mo ago
    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?
    - wavemode 11mo ago
      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).
- voxl 11mo ago
  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?"
- ashton314 11mo ago
  > … 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.
sriku 11mo ago
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.
- sriku 11mo ago
  Am working on rewriting an imperative programming course to use Dafny to present verified algorithms and data structures.
  - fithisux 11mo ago
    Please post HN when you finish.
mikiskk 11mo ago
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/fall2024/ https://glados-michigan.github.io/verification-class/fall202...
skybrian 11mo ago
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?
tgv 11mo ago
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?
- csb6 11mo ago
  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.

110 points by handfuloflight 11mo ago

dionian 11mo ago

Reminds me of Eiffel, in a good way. Looks awesome. Is there anything close to this in Scala by chance?

gz09 11mo ago
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).
- ted_dunning 11mo ago
  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.
- esafak 11mo ago
  This expressiveness is a curious point, because a common charge leveled against Scala is that it is too expressive.
  - steego 11mo ago
    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.
ted_dunning 11mo ago
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.

fjfaase 11mo ago

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?

algorithmsRcool 11mo ago
It could be done, but what would be the virtue of it? Most programming languages are not self-hoisted for a reason.
- fjfaase 11mo ago
  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.
deleted 11mo ago
[deleted]

fooker 11mo ago

This might be a stupid question, but why a separate programming language rather than aiming to verify/synthesize invariants in languages people use?

quamserena 11mo ago
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.
- fooker 11mo ago
  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?
  - wavemode 11mo ago
    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).
voxl 11mo ago
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?"
ashton314 11mo ago
> … 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.

sriku 11mo ago

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.

sriku 11mo ago
Am working on rewriting an imperative programming course to use Dafny to present verified algorithms and data structures.
- fithisux 11mo ago
  Please post HN when you finish.

mikiskk 11mo ago

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/fall2024/ https://glados-michigan.github.io/verification-class/fall202...

skybrian 11mo ago

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?

tgv 11mo ago

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?

csb6 11mo ago
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.