alt Hacker News> My reason: code can be checked objectively. I can run it and confirm it works.
Running the code only confirms that it works with the precise input, in the precise environment, under the precise circumstances you run it under. It doesn’t ensure that the code is correct. Thinking through the code, on the other hand, lets you consider all possible cases. It’s the difference between experiment and (mathematical) proof.
For an objective correctness proof, using a formal language is indispensable.
Replies
Even thinking through the code is not complete because our brains make mistakes. They also make assumptions, thousands of them, that you don’t know about. It’s tricky, because every thought you have has an entire sea of preconceived notions and knowledge behind it, which you can’t identify. In that way, it’s similar to an LLM.
In practice, for code, testing code is the way to go. Formal proofs work, too, but the barrier to entry is high and it’s overkill for most business applications. LLMs can be very good at writing tests, if you read the test thoroughly and analyze them.
Code is a formal language, and can be partially (or rarely fully) verified by a typing system. There is no equivalent in natural language.