The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Have you examined the most recent incarnation of F* 
(https://www.fstar-lang.org)?  It now seems to be roughly equivalent to 
Coq/Agda/Idris in terms of type system power (fully dependent types, 
instead of F*'s original value-dependent types) - and it uses the Z3 SMT 
solver as part of its built-in automation.  I'm just starting to examine 
it myself - encountering the typical issues involved with immature 
systems.  Also, F* currently seems to lack many of the friendly features 
of Coq - such as interactive proving, a proof mode, a tactic language, 
and PG-like IDE support.  But, F* seems to make a case for SMT in the 
type-checker/proof-assistant world - beyond merely being an alternate 
source (vs. plugins and Ltac) for restricted-domain decision procedures 
(although there's certainly nothing wrong with that).

What I'd like to see is for there to be a way to use SMT-like algorithms 
within Coq to enhance its automation tactics (auto and friends) beyond 
doing proof search solely by trial-and-error.  I don't know if F* uses 
Z3 for something like that, or has plans to.

-- Jonathan