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.
I'd have assumed, by virtue of being Turing complete, you could express any invariant in almost any language?
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).
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.
I assume if you were to develop such a system for C, C++, or Rust you'd similarly expect the user to do this.
(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.
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.
As for being not expressive enough for specifications, isn't the code itself a form of specification? :)
Dafny can compile to and interface with a few languages, including C#.
Are there benchmarks showing dafny is faster than other inefficient options ?
I'm not sure about benchmarks comparing languages, but Dafny goes through a lot of tweaking to make the process faster.
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
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.
https://glados-michigan.github.io/verification-class/fall202...
Fine for teaching, but it doesn't seem to be a suitable tool to generate idiomatic library code?
dionian•1mo ago
gz09•1mo ago
ted_dunning•1mo ago
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•1mo ago
steego•1mo ago
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•1mo ago
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.