Hacker News Reader

> but they are not actually similar structurally.

The Curry-Howard isomorphism wants a word.

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.

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