Re:Dafny – A programming language with a program verifier
by tom_mellior on Friday January 20, 2017 @06:59AM
(#13443180)
> I'm thinking there must be a reason they do not mention F* , Coq, Agda, and Idris
The ones they do mention are all imperative languages with added deductive verification in a Hoare calculus style (think loop invariants). The ones you mention are functional languages with a different style of proof (think inductive proofs).
Of course there are overlaps between the two styles (notably in Why3), but there are pronounced differences between them.
The ones they do mention are all imperative languages with added deductive verification in a Hoare calculus style (think loop invariants). The ones you mention are functional languages with a different style of proof (think inductive proofs).
Of course there are overlaps between the two styles (notably in Why3), but there are pronounced differences between them.