2 ms·
I encourage you to try Metamath. When starting a new axiom system from scratch, I found that I was not capable of writing anything that would cause lag; I wasn'
by lidHanteyk 7y ago
I encourage you to try Metamath. When starting a new axiom system from scratch, I found that I was not capable of writing anything that would cause lag; I wasn't able to make Metamath the slow part of my workflow. No matter how I approached it, the slowest parts of my work were my typing (with my fingers) and my typing (with my mind and whiteboard).
No other formal proof assistant has been this fast for me. The next closest one is Idris, which is type-theory-driven (fancy phrase for "slow") and it takes a few moments to round-trip between the REPL and the text editor.
- h91wka 7y ago> the slowest parts of my work were my typing My rule of thumb says: if fingers are the bottleneck, then your programming language is not powerful enough (too verbose). Working with higher level abstractions is good for health: brain doesn't get RSI. > which is type-theory-driven (fancy phrase for "slow") ...
- digama0 7y agoWhat if your brain is the bottleneck?
- lidHanteyk 7y agoSyntax-only formalisms are faster than semantically-laden formalisms; a compiler's parser is usually faster than its backend. Metamath is going to always be faster than Coq, Lean, Isabelle, HOL, Agda, Idris, or indeed much weaker systems like Haskell. There's no RSI in working with Metamath. What I mean is that the workflow is largely dependent on me knowing what I want to prove and roughly how I want to prove it, rather than Metamath chewing CPU.