3 ms·
Theorem proving doesn't require immutability it anything like that—its requirements are far more severe. Your language must have at least some fragment which is
by tel 12y ago
Theorem proving doesn't require immutability it anything like that—its requirements are far more severe. Your language must have at least some fragment which is the internal proof language of a complete and consistent type theory! This is why, for instance, these languages are always Turing incomplete.
- tomp 12y agoHm... I'm not so sure about that. Of course, if we're speaking about dependent types, then yes. However, theorem proving could also be done automatically, by an external theorem prover, which would only need the refined type annotations on your variables to prove stuff (using the whatever theories the theorem prover knows about, such as linear integer mathematics, logic, real nonlinear math, vectors, datatypes, etc).
- tel 12y agoThat can happen sometimes for some theories. It's super easy to run into places where proof search fails magnificently.