News for hackers. Stuff that matters.

A comment on Dafny – A programming language with a program verifier. Parent comment

Re:Dafny – A programming language with a program verifier by igravious on Friday January 20, 2017 @06:38AM (#13443087)
Per the Wikipedia page for Whiley[1] the languages akin to Dafny are mentioned when explaining what Whiley is: “The primary purpose of such a tool is to improve software quality by ensuring a program meets a formal specification. In other words, to help identify and eliminate software bug in the programs being developed. Whiley follows many attempts to develop such tools, including notable efforts such as SPARK/Ada, ESC/Java, Spec#, Dafny, Why3 and Frama-C.”

I'm thinking there must be a reason they do not mention F*, Coq, Agda, and Idris, perhaps because they are proof assistants[2] rather than automatic provers of programs with formal specifications. See also Isabelle and others. Regarding Idris (which you mention but is not on that page) and Epigram (which is noteworthy and again not on that page), neither are production ready and the latter is unmaintained.

[1] https://en.wikipedia.org/wiki/Whiley_(programming_language)#...

[2] https://en.wikipedia.org/wiki/Proof_assistant

[ Parent | on HN ]
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.

[ Parent | on HN ]
Re:Dafny – A programming language with a program verifier by igravious on Friday January 20, 2017 @08:09AM (#13443502)
Ok. But that's not what I was getting at.
[ Parent | on HN ]