Think about the filesystem, the big issue with formalizing a program spec that operates on a file system is simply the fact it is essentially a shared object amongst all the programs running on the system. Add to that the fact that (though this changes with modern containerization systems, namespaces, pledge what ever) a program may at any point gain access to root permissions if it makes the system call to do so providing the correct credentials it becomes very difficult formally be able to remove any possible states from the system.

All this could be different but we would radically need to redesign are systems and the way we think about the problems.

While these areas were main premise of an article when it was written, I think the article really aged well into current time of mass AI/LLM deployment. It shows fundamental limitations of token based systems / symbolic reasoning that LLM espouses internally, while writing correct software. These limitations also apply to humans, however humans mental modelling, being not fully based on symbolic processing, have been historically shown capable of writing correct software systems, while AI/LLM systems have not been proven to be able to do that, and as article shows that with current token based technology it's unlikely they will ever be.

This does not require proving systems complete correct, but it does involve proving many properties of these systems.

Some API:s can be perfect. But then the real world adaptation needs to happen inside the module serving the API.