4 ms·
> but they are not actually similar structurally. The Curry-Howard isomorphism wants a word.
by epgui 4y ago
> but they are not actually similar structurally.
The Curry-Howard isomorphism wants a word.
- xor99 4y agoTrue, I guess as the other commenter has pointed out there is a huge difference between scripting languages and their seeming closeness to natural language compared to mathy languages like Haskell that have this isomorphism and are very structurally similar.
- epgui 4y agoA less type-safe language would still be isomorphic to a mathematical proof, but it could contain a wider range of errors compared to a more type-safe language. The language could be either functional or imperative, and still be isomorphic to a proof. A correct (error-free) computer program written in any language (even javascript) would be equivalent to a correct mathematical proof. It's a bit mind-bogglingly profound, but that's the beauty of the Curry-Howard correspondence.