[ipnon]

One of the benefits of the Curry-Howard isomorphism is that people like myself who never make anything useful can use computers too.