All types in Turing complete languages are inhabited by non terminating terms (looping forever, throwing exceptions), which means all propositions are provable.

All types in Turing complete languages are inhabited by non terminating terms (looping forever, throwing exceptions), which means all propositions are provable. For instance in Typescript, const absurd = <A>(): A => absurd() const unimplemented = <A>(): A => { throw new Error(“Unimplemented”) } const uninhabited: string & number = absurd() Intuitively you can think of it like, “Yeah sure, I can build you a term of any possible type, as soon as I get back to you.”, but then the function just ghosts you by looping forever. But it hasn’t lied. However, so long as you’re aware of these gotcha’s they don’t come up much in practice which is why viewing types as proofs is still useful. Just don’t stake your career on one.