Comment by moritzwarhier

> The problem that needed solving: Computer programs make mistakes because they're too literal and they don't understand a programmer's intentions.

> The problem they tried to solve instead: Computer programs make mistakes because we don't write out mathematical formulas detailing how programs should behave, and mathematically prove that our programs obey said formulas.

The problem is documenting the intent of a rule-based system and confirming that it acts as expected.

As every programmer knows, thoroughly defining intended behavior is the meat of impmenting said behavior.

Often refining the intent based on thinking through or implementing intermediate solutions.

This is not just because of the difficulty to make computers behave the way we want to, it includes the difficulty of defining how we want it to behave, too.

There is no silver bullet that can remove ambiguity from human instructions, or always guess "correctly" when missing clear instructions.

Because by definition, what is correct?