Hacker News Reader

True, 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.

View on HN

A 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.

Reply on news.ycombinator.com