3 ms·
> 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
by 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.