This keeps bringing me back to John Backus’s Turing award lecture/paper, “Can Programming be Liberated from the Von Neumann Style?”

In it he pointed out a huge deficiency of most programming languages that still haunts us: they’re wickedly difficult to reason about. So proving important properties about programs is all but infeasible.

So we try to handle it empirically with unit tests, but that has its limitations.

LLMs can kinda sorta do it analytically, but that isn’t completely satisfying, either. The results are probabilistic, and they are pretty bad at inferring intent which can be a source of both type I and type II errors. But still, it would be silly to throw out a layer of Swiss cheese for having holes.

But I sure do wish we could have a plausible version of Backus’s original vision of a language that lets us formally declare (a useful subset of) the specification and then statically verify that the program conforms to it.