Dafny: Verification-Aware Programming Language
1–10 of 35 posts
Re: Dafny: Verification-Aware Programming Language
#2Reminds me of Eiffel, in a good way. Looks awesome. Is there anything close to this in Scala by chance?
Re: Dafny: Verification-Aware Programming Language
#3Looks interesting. I saw some C# files, from which it seems it is implemented in C#. Is there going to be an implementation in Dafny?
Re: Dafny: Verification-Aware Programming Language
#4Reminds me of Eiffel, in a good way. Looks awesome. Is there anything close to this in Scala by chance?
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).
Re: Dafny: Verification-Aware Programming Language
#5Reminds 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.
Re: Dafny: Verification-Aware Programming Language
#6This might be a stupid question, but why a separate programming language rather than aiming to verify/synthesize invariants in languages people use?
Re: Dafny: Verification-Aware Programming Language
#7Reminds me of Eiffel, in a good way. Looks awesome. Is there anything close to this in Scala by chance?
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.
Re: Dafny: Verification-Aware Programming Language
#8This might be a stupid question, but why a separate programming language rather than aiming to verify/synthesize invariants in languages people use?
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.
Re: Dafny: Verification-Aware Programming Language
#9This might be a stupid question, but why a separate programming language rather than aiming to verify/synthesize invariants in languages people use?
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?"
Re: Dafny: Verification-Aware Programming Language
#10This might be a stupid question, but why a separate programming language rather than aiming to verify/synthesize invariants in languages people use?
> … 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.