Our approach shouldn't be to give up striving for better programs, algorithms, and code. Despite our current inability (which I don't think is a failure of programmers but business decisions), we can nevertheless reject further opportunities for decline, in name of profits, right?

That is not what I said. Of course we should strive for precision, corectness etc. but that does not mean that current and future imprecise methods of development do not hold any value. There is plenty of value to be gained from poorly written software which we will keep writing until we get magically verified ones.

We don't write formally verified code because writing the code to pass the verification is annoying and hard. If we're only writing the formally verified spec and a program or AI generated the code, that's a bit easier, though it may have to get easier still before it becomes mainstream.

> I cannot do this

You could if you wanted to. You're smart, inventive, and creative. There's nothing stopping you from learning.

> Why would a tool need to be formally verified to be considered impressive and/or useful?

Part of it depends on your perspective.

If we assume that an LLM (or some future ML tool based on it) is capable of producing code with the same rate of errors as a trained, expert human could then it would seem the productivity gain is not having to write all of that code ourselves.

We already tolerate a certain amount of errors in our software and the world has not collapsed. The JVM had an error in its binary search implementation that lasted for nearly a decade before anyone noticed. They noticed because the size of the arrays being used started getting big enough that their programs started failing in mysterious ways. OpenSSL had a vulnerability that sat unnoticed for more than a decade. The cost of errors is not zero but it is tolerated.

However the problem of programming is that we think it's our ability to write code which is the problem that is slowing us down.

My perspective is that we're not focusing on the problem: that it is hard to be precise and write programs that work, whole cloth, from their specifications without any errors.

Using an LLM to generate more code has another problem: while humans are decent enough at writing code to solve our problems, even if our solutions are imperfect, we're far worse at reading code and understanding what it does and whether it is correct with regards to some specification (if there is one).

Empirical studies of large-scale code review are very humbling. We can read maybe 200 SLOC every couple of errors and have a negligible impact on error rates in the software being produced. More than that and the effect disappears.

So now we have LLM's producing code that we know will have errors in it. And we have no idea where the error is. It could be a trivial error we could tolerate. Or it could be another Bar Mitzvah CVE. Hard to say.

Even Betrand Meyer missed an error in a single-line expression generated by ChatGPT. He's way smarter than me. I don't see how we'll be able to keep up.

But if we tackled the problem of getting better at being more precise with our specifications, I could definitely see how having an AI-like system automate code generation being really useful. There are plenty of times when working on a formal proof where you want to say, "this is obvious!," that have a machine verify that for you using the same proof rules and tactics you would use. Bonus points if it can explain the proof back to you.

I just think we're a long way off from being able to do that.