But there wasn't enough demand and it was discontinued.
"I decided for myself that X wasn't worth me pursuing as a path for my career." Good for you.
I made the same decision for professional photography and cardiac surgery, but both of those careers still hold value to society.
The problem here is that the correct amount of resources is context-dependent.
Suppose you're a small business and you're putting up a website to display the menu for your restaurant and directions to get there. Do you want it to get compromised? Of course not. Does it matter very much if it does? Eh. Should you spend $50M in formal verification to make sure it doesn't? Definitely not.
Whereas if you're developing the software that keeps planes from falling out of the sky, that's an entirely different context.
The problem comes when someone grabs the awful WordPress junk that was suitable for displaying static menus and wants to use it to process credit cards. But even that isn't really the fault of the awful WordPress junk, it's the fault of the credit card companies for designing their financial technology in such a ridiculous way that Merchant A has to be given a secret that allow purchases to be made against the same card at Merchant B, instead of using the decades-old cryptography that would prevent the customer from ever needing to give anyone a secret that enables that wide a scope of compromise.
It comes down to how much work is justified to ensure that the thing not have problems, which is not at all the same across different domains.
You're right about approximations: we gather data and improve theoretical models in an attempt to exhaust that complexity reality poses.
You're wrong about exhaustive knowledge about codebases being impossible. LLMs enable exactly that.
The trick then is to transfer that knowledge in a usable way to what we know about the codebase.
I agree with the necessary cultural shift.
It doesn't actually give you the truth of a statement, it just convinces a mathematician of its truth.
That doesn't actually change when computers are brought into things. You can convince a mathematician that an automatic theorem prover constructs correct proofs with another proof, but it's "I think this looks right" all the way down.
Mathematicians are trained to act as the compiler, verifying the code, doing the type checks, and to a degree the state machine "running" those programs.
Human mathematicians use introspection to tell you whether a proof/program does what it is supposed to do. They keep those programs small enough to be run on human brains by modularization, abstracting away complexity behind defined interfaces. They mostly rely on other mathematicians to have checked those sub-modules properly.
By defining that state machine, compiler and the tree of "all" known proofs as programs explicitly on a computer, you get Lean and the according libraries of verified proofs.
A proof-program there is verified when it compiles and passes the deterministic structural type-checks built into the language while fulfilling the requirements stated for its interface.
It all reduces to a few thousand lines of trusted code, the Lean kernel, being correct. It's mostly what humans do too, but actually considerably more thorough.