|
|
|
|
|
|
by jonsterling
3825 days ago
|
|
|
It'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. |
|
|