That doesn't seem sustainable. It also seems like a poor cost to value ratio.
That doesn't seem sustainable. It also seems like a poor cost to value ratio
Those "prove" you see in academic paper are very specific case.
And I don't know why you put "prove" in scare quotes. There is formally verified software that has been proven to conform to a spec. They aren't just toy programs either, see SEL4 or CompCert for 'real' programs.
Fully verified programs do exist (e.g. CompCert C compiler), although for various reasons, it's still a niche.
> Those "prove" you see in academic paper are very specific case.
Not to put too fine a point on it, but every program written is a very specific case, so I'm not sure this is such a convincing point.
As you say, there is absolutely, provably, no general-purpose algorithm out there that will prove program correctness automatically. That is in no way to say that humans can't or shouldn't try to prove some programs correct, or even that you can't have an algorithm that will prove certain classes of programs correct.
With that said, I do also think your parent:
> We have figured it out. People with a PhD and given enough time can do it. Scaling this will be possible, especially with the help of AI, as soon as there is the actual will there to do it.
is too optimistic, and throwing a little cold water on that rosy prediction is appropriate.
Aren't we already there outside of very specific special applications? At the very least you have to assume every library you are using and the framework you are running on is correct. Sure, that works 99.9% of the time. If your testing framework can get the rest of the code to 99.5% of the time, is the .4% that large of a deal in a case where the other .1% is not?
When we look at what the market wants, what individual people want, do they want things proven correct given the increase in cost it brings? They may say they do, but spending behavior doesn't seem to align.
pretty much every domain, if you exclude finance & industries that intersect with life and death decisions such as pharma/medicine/airlines/defense.
what’s the correct order of movie recommendation ? its easy to see that given your past netflix history, there is an obviously incorrect order. but there is no obviously correct order - any number of orderings will work. correctness is not paramount.
what’s the correct puzzle to assign to a 1400 on chess.com ? obviously there are hundreds of them that would work. correctness is not paramount.
what’s the “correct price” of a used Ford Focus ? depends on whether you are a bandit who needs the car for a rapid getaway, or whether you are the brother in law of the used car salesman, in which case the correct price is zero usd.
the sole reason why 100 million developers crowd the web programming circuit and not other gatekeeped domains is because correctness is not paramount. whether your color code is off by a shade on this browser or your pixels misaligned on that browser, its all fine so long as it somewhat works. correctness is not paramount. otherwise nothing would ship.
Note that people die if data is lost, causing companies to go bankrupt (suecide). But really, not everything has to be correct, look at Intel and AMD. They've been compromising correctness for speed for quite awhile, and we're mostly fine.
EDIT: I assume from your comment that you formally verify every line of code in every system you depend on, and run RISC-V to make sure the hardware doesn't tamper with your instructions.
I suspect this to be the majority of code written.
Then when every program is eventually upgraded to this status, all of the code we run is bootstrapped through proprietary AI - including the AI itself - and it's black boxes all the way down. Programming is now an experimental science where we gather evidence, test hypotheses, press the "copilot" button and tune parameters, like evolutionary biologists studying DNA code.