function prove_anything<P>(){
function prove_false() : False {
return prove_false()
}
let f = prove_false()
return contradiction<P>()(f)
}
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.
(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: https://www.typescriptlang.org/docs/handbook/type-compatibil... :)
It's still fun to see how far we can take an unsuitable type system like that of TypeScript for formal verification.
This typechecks:
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.(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: https://www.typescriptlang.org/docs/handbook/type-compatibil... :)
It's still fun to see how far we can take an unsuitable type system like that of TypeScript for formal verification.
I just notice now that I wrote is a suitable alternative. I meant to write is NOT a suitable alternative. :)