| ▲ | dvt 39 minutes ago | |
Imo, this is like saying "I judge a carpenter based on how straight they can cut a piece of plywood." Or like saying "I judge an artist on how accurately they can draw a circle by hand." I mean that's certainly one way of looking at it, and both can be impressive technical feats. But most people judge carpenters and artists on their end products, their overall vision, their motifs, their philosophy, and so on. On the other hand, as a trained logician, I definitely see proofs (which, by the Curry–Howard isomorphism, are computer programs) have some degree of beauty-within-themselves, but that's quite hard to achieve. Not everyone is a Gödel, after all. I also think programming languages, despite being Turing complete (which is frankly not saying much), are far too limiting to truly construct magnificent things with. | ||