alt Hacker News> The vast majority of it could be inscrutable, ugly, chaotic and seemingly meaningless.
It is, provably: per Curry–Howard correspondence, any program you write is a proof of a theorem, and it is indeed mathematically meaningless.
> The vast majority of it could be inscrutable, ugly, chaotic and seemingly meaningless.
It is, provably: per Curry–Howard correspondence, any program you write is a proof of a theorem, and it is indeed mathematically meaningless.
Generating a value of type "Either (Int, String) Bool" is proving that there's at least one integer and at least one string, or there's at least one valid boolean value. Except in Haskell, where it could also be an infinite loop.