The Coq mailing list

[Claude Marche <Claude.Marche AT inria.fr>]

I think I agree with you on all of your points except :

Le 18/05/2015 13:00, Soegtrop, Michael a écrit :
> What I don't like are approaches which try to map everything to SMT, like 
> Dafny.

Dafny does not map everything to SMT. Look at the concept of lemma
functions in Dafny, this can be used to prove quite complex mathematical
properties, in particular those requiring inductive reasoning, by using
the programming language to build a kind of proof skeleton. Similar
constructs exist in similar tools like Why or VeriFast. For Why3, it
appears to be a very handy alternative to the use of the Coq back-end.

- Claude


-- 
Claude Marché                          | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France           |
Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |