4 ms·
Is there any reason to single out Nuprl for this though? We could slap SMT onto a wide range of elaborators (as it has been a stated goal for the Lean prover, a
by Kutta 11y ago
Is there any reason to single out Nuprl for this though? We could slap SMT onto a wide range of elaborators (as it has been a stated goal for the Lean prover, and there has been attempts in Isabelle, Coq and Agda too if I recall correctly). Practical elaboration already involves a large amount of machinery that isn't reflected in kernel type theory, so I don't see why Nuprl would be better in this regard.
- jonsterling 11y agoIt's a matter of behavioral type theory vs structural type theory; each can benefit from "slapping a solver on", but behavioral type theory allows you to reason directly about the code from a partial and effectful language, whereas structural type theory does not (in a direct way, at least). Lean, Coq and Agda all implement structural type theory.