About 15 years ago, I was hanging out at the MIT AI Lab, and there was an ongoing seminar on the Coq proof assistant. The idea was that you wouldn’t have to guess whether your programs were correct; you could prove that they worked correctly. The were just two little problems: It looked ridiculously intimidating. Rumor said that it took a grad student all summer to implement and prove the greatest common divisor algorithm, which sounded rather impractical. So I decided to stick to Lispy lan...
