The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Benjamin,

> According to Leo's talk at the recent CPP workshop, lean does not use Z3 
> itself, to avoid awkward encodings of type theory in FOL. 
> However, he says that almost all of the techniques used in Z3 can be 
> adapted fairly readily to type theory, so most of Z3 will be in some sense 
> built in.  

thanks for the information! So I guess some of the people working on Z3 also 
work on Lean. This is an interesting development. I wonder what this means 
for the future of directly Z3 based verification tools like Dafny.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928