Dafny is a programming language with a program verifier. As you type in your program, the verifier constantly looks over your shoulders and flags any errors. Dafny is currently spread across 3 sites:

Read more:
The language itself draws pieces of influence from:
  • Euclid (from the mindset of a designing a language whose programs are to be verified),
  • Eiffel (like the built-in contract features),
  • CLU (like its iterators, and inpiration for the out-parameter syntax),
  • Java, C#, and Scala (like the classes and traits, and syntax for functions),
  • ML (like the module system, and its functions and inductive datatypes), and
  • Coq and VeriFast (like the ability to include co-inductive datatypes and being able to write inductive and co-inductive proofs).

External contributions:

Last edited Apr 1 at 10:45 PM by rustanleino, version 9