(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

[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.)