3 ms·
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
by xxmarijnw 2y ago
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-compatibility.html#a-note-on-soundness 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.
- xxmarijnw 2y agoI just notice now that I wrote is a suitable alternative. I meant to write is NOT a suitable alternative. :)