1 comments
This typechecks:<p><pre><code> function prove_anything<P>(){
function prove_false() : False {
return prove_false()
}
let f = prove_false()
return contradiction<P>()(f)
}
</code></pre>
I think a proof assistant will usually have a total notion of computation to avoid this kind of circular proof. And there are probably some subtler unsoundnesses in TS to worry about.<p>(I'm not any kind of expert in this area. It's possible the original author intends that you execute the proof function as well as typechecking it, which I guess will prove termination, although I think for many proofs you might run out of resources trying to do that, and it's probably still not sound.)
TypeScript is a suitable alternative to real proof assistants like Rocq. Not only does non-termination break Curry-Howard like you mentioned, the type system of TypeScript is actually unsound on purpose: <a href="https://www.typescriptlang.org/docs/handbook/type-compatibility.html#a-note-on-soundness" rel="nofollow">https://www.typescriptlang.org/docs/handbook/type-compatibil...</a> :)<p>It's still fun to see how far we can take an unsuitable type system like that of TypeScript for formal verification.