(no subject)

[gusl]

IMPS (An Interactive Mathematical Proof System), thanks to Freek Wiedijk for the reference!

In contrast to the formal proofs described in logic textbooks,
imps proofs are a blend of computation and high-level inference. Consequently,
they resemble intelligible informal proofs, but unlike informal
proofs, all the details of an imps proof are machine checked. imps emphasizes
interactive proof development. There is essentially no structural
dierence between completed proofs and partial proof attempts.

This is exactly what I've been asking for... not only does it provide interpretations, but it's also interactive. High-level proving.

I wonder if the mainstream of the Formal Mathematics community is using the analog of Assembly languages.

Comments

Re: Assembly

[gustavolacerda.livejournal.com]

Indeed, lambda-calculus as used in LCF and its descendants (HOL, Coq, etc.) has been dubbed "The Assembly language of proof systems".
by whom?

I don't know the system yet. The only idea I have is that it would be more natural to work in the language of the specific area... e.g. group theorists would like to work in the language of group theory, instead of in type theory. (I'm not sure though if this makes a significant difference to the group theorist)

This language is then translated (i.e. "faithfully interpreted") into the low-level language of the foundation (type theory, set theory, whatever).

I wonder if this is why current formalization work takes so damn long.

I'm just surprised that I hadn't heard of IMPS before. If it's that much better than the mainstream, people would be using it... so I wonder if there's a catch...

Btw, I've mentioned you in my revised proposal. http://student.science.uva.nl/~glacerda/FormalizingScienceIntuitively/
Comments are always welcome.

Re: Assembly

[selfishgene.livejournal.com]

I suspect the catch is, that it is still hard work to make worthwhile proofs, notwithstanding a good method of developing/describing them. (This statement is made after 30 seconds of analysis, so it may be total shit.)