Isabelle

[fl]

In my opinion, Isabelle is the better example of what musn't be done in terms of proof assistant:

+ Obscure non documented framework.

+ No explanation of the underlying logic.

+ Intermangled syntax.

+ A tutorial that explains that to prove something you apply "auto".

+ A strategy of explanation that can be summed up by "let's begin in the middle, it's clearer."

+ And the icing on the cake: final proofs that can't never be examined in details. You simply don't know why it is proved.

Maybe I'm the only one who has this opinion.

--
FL

[Mario Carneiro]

I was blown away when I discovered that Isabelle's proof of the prime number theorem was done in Isabelle2005, and it was not upkept along with the AFP (archive of formal proofs). Moreover, apparently not even the creators know how to run Isabelle2005 anymore, and everything has changed since then so it's not backward compatible by any stretch. Basically, the proof is lost at this point, and they are more likely to formalize an entirely different proof than upgrade the one they already have.

I really don't want this to happen in Metamath.

Mario

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Stefan O'Rear]

Sometime around 2007 I got the formal proofs bug for the first time.
I tried Coq (which I got somewhat working), as well as Isabelle and
Twelf which I didn't understand well enough to use. Plural of
anecdote is not data, etc. Then in 2014 I got the bug again and went
specifically looking for a proof assistant based on "normal" first
order ZFC, Mizar looked cool up right until I discovered there were no
public sources, then I found Metamath…

-sorear