I was initially excited about this; a prover with a logic like Coq (dependent types!) but with awesome extensions (effects!) and with the automation of Z3 seems pretty neat. I decided to test-drive it with the first few chapters of the Software Foundations book (<a href="https:&#x2F;&#x2F;www.cis.upenn.edu&#x2F;~bcpierce&#x2F;sf&#x2F;current&#x2F;index.html" rel="nofollow">https:&#x2F;&#x2F;www.cis.upenn.edu&#x2F;~bcpierce&#x2F;sf&#x2F;current&#x2F;index.html</a>).<p>Now, I must admit, I&#x27;m a lot less excited :-( You can see my results for (almost all of) the first two chapters here:
<a href="http:&#x2F;&#x2F;pastebin.com&#x2F;5bL7Wugq" rel="nofollow">http:&#x2F;&#x2F;pastebin.com&#x2F;5bL7Wugq</a> <a href="http:&#x2F;&#x2F;pastebin.com&#x2F;GRFLCF8Z" rel="nofollow">http:&#x2F;&#x2F;pastebin.com&#x2F;GRFLCF8Z</a><p>Unfortunately, proving in F* turned out to be a pain. The basic problem is that during proving you have no idea at all about the state of the proof; the only way I could get anything done when automation failed (and that was more often than I had hoped) was by working out, in comments, a very detailed proof, and then applying appropriate lemmas. If you know Coq, think of it as writing down tactics <i>without seeing the proof state in the side pane</i>, and having to get it complete before you get a simple yes&#x2F;no answer telling you whether what you did was good enough to make the entire proof go through. But in fact, it it is even more painful than that: In Coq, you can apply&#x2F;rewrite with lemmas just by naming them, but in F* you need to instantiate all arguments. So a proof step for one of the lemmas in the second document above, which would be <i>rewrite -&gt; plus_swap</i> in Coq, in F* must be written <i>plus_swap n m&#x27; (mult (S n) m&#x27;)</i> although Z3 could easily find the correct arguments itself. But leaving arguments off is simply not possible in a system of this kind based on the notion that a &quot;proof&quot; is written a well-typed program.<p>Oh well. Back to Isabelle&#x2F;HOL for my regular theorem proving needs, although its logic is really weird and I wish there was some system combining the automation of Isabelle with the Calculus of Constructions.