I sense some confusion here. Let's define our dictionary first. IDE is just a text editor with UI for syntax highlighting, autocompletion, code and documentation searching and integrating other stuff. It also has to be fast and robust. Verifier should just check soundness of definitions, wellformedness of terms and correctness of proofs. Working incrementally is a big advantage. Proof assistant should enable automated synthesis of proofs by inferring missing information, automatically coercing terms, filling in gaps and making good suggestions (according to Andrej Bauer).
mmj2 has a very basic IDE with integrated verifier. It's also a very rudimentary PA as it has only a simple unification tool for synthesis. Granted, there are some basic tactics written in JS but it isn't suited at all to be programmed by an average user. It's also buggy, slow and monolithic, it can't be easily used from other projects. I believe that's what prompted Mario to start this thread in a first place, right? There is also an established tradition to write PA in a functional programming language. -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/51c47b52-88de-48ee-9be4-4d48d615f2c2n%40googlegroups.com.
