Try asking a programmer to provide a formal proof of correctness of even a simple algorithm. Most are not trained to do this. Many try to forget it when they le

Try asking a programmer to provide a formal proof of correctness of even a simple algorithm. Most are not trained to do this. Many try to forget it when they leave academia. Few actually try to use it. Expecting a human to disambiguate and do nonsense filtering is a crap shoot. Usually done through trial and error. We write things we think are correct according to an informal specification and since there’s no way to prove our implementation is incorrect… we review it, wrote a few example tests, and deploy it. Surprisingly this is good enough most of the time because the liability for mistakes lies with the company, most mistakes are benign, and users will tolerate being frustrated to a degree. This is why I’m not optimistic about LLM’s replacing programming. The art and science of programming is rooted in formal mathematics. It takes a sophisticated ability to reason and a certain amount of creativity to write beautiful proofs. And formal maths demands a level of rigorous thinking that even mathematicians balk at. The allure that EWD is writing about here is very much alive. Many people hope to have a genie inside their computer do the thinking for them. It may not be the answer we desire but precise thinking is what we need and I would rather have better tools and languages for doing formal mathematics and programming with them than using a really expensive system to piece together the program I want from other peoples’ code and guessing what I want from an imprecise specification. If the specification itself isn’t precise then any program I give you, by definition, cannot be wrong.