Hacker News Reader

Comment by fouronnes3 | Hacker News Reader

It's interesting to me that the next few steps of this technology evolution might be that we loose the ability to prove our code correctness forever. Every program will just be a certain - measured by tests - percentage of accuracy against some goal and that's it.

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.

View on HN

Can't say we've really figured out proofs for program correctness now, can we?

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.

I admire your optimism.

So, for people to quickly implement http requests, we need a mountain of AI hardware backed by legions of PhDs with endless time to vet the http requests.

That doesn't seem sustainable. It also seems like a poor cost to value ratio.

No. If it is something that has been done plenty of times before, then we would also know how to prove the correctness of it automatically. It would also lead to much better and less code, because you would be aware that it has been done before so many times.

So, for people to quickly implement http requests, we need to feed, clothe, and discipline humans for a minimum of two decades, backed by legions of teachers, doctors, and professors with endless time to service them.

That doesn't seem sustainable. It also seems like a poor cost to value ratio

Proofing correctness (in general) is incomputible (halting problem and stuffs).

Those "prove" you see in academic paper are very specific case.

> Proofing correctness (in general) is incomputible (halting problem and stuffs).

> 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.

Thankfully correctness in the general case doesn't matter in reality, in the same way that it doesn't matter that not all 'correct' programs can be possibly typed.

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.

The halting problem doesn't prevent you from writing proofs for programs, same as Gödel's theorems don't prevent mathematical proofs from existing.

Fully verified programs do exist (e.g. CompCert C compiler), although for various reasons, it's still a niche.

We haven't even figured out how to specify what "correctness" means for all but the most trivial examples. What is the "correct" behavior of that example snippet in the linked post?

Very good question! Try to figure it out yourself and you will see what is wrong with software development today.

I don't know anything about formal correctness proofs but my imagination tells me it is bounded by the description of the task. Aren't we just shifting the bugs toward the task description? Or is it about being able to specify a task with a very simple program (e.g. brute force) that is unfeasible to run but can be somehow used to verify that simpler (in terms of runtime complexity) programs provide the same outputs?

Yes. Figuring out what a program SHOULD do is often as hard as figuring out how to actually do it. The relative difficulty shifts depending how far you are from the real world. The closer your project is to actual people doing actual work, the harder it is to define the requirements precisely.

Sure, if your task description/specification is buggy nothing can save you, but if you only have to check the spec your work gets much easier. If you write a program, you have to both make sure that the spec is correct and that the spec is correctly implemented.

Yes, they can only logically deduce correctness based on our assumptions of a given system boundary. But I think it is typically a good idea to write them down formally if you need the guarantees. They are also typically smaller and more declarative.

>It's interesting to me that the next few steps of this technology evolution might be that we loose the ability to prove our code correctness forever. Every program will just be a certain - measured by tests - percentage of accuracy against some goal and that's it.

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.

All programming though ? That's a stretch. Like I'm pretty sure there are domains where correctness of programs is paramount

Is there a domain where correctness is not paramount?

If people don't die from your mistakes they're not important IMO.

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.

Yeah because losing money, market share or people’s data is fine ?

Depends on the numbers, if my company loses 10k because i made a mistake nobody would "care". Mistakes happen to the best of us, which is obviuous looking at public CVE's. If it's 100k it'd be a different story, considering we're not that big (35 employees). It's just money, it can be replaced, human lives can't.

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.

Computer graphics maybe? You can shift goal posts what "correctness" means, but if a game renders something in a funny way, it's really not going to hurt anyone. Yes, if it's constantly a total mess nobody will want to play the game, but 1. that would be (presumably) found quickly during testing, and 2. this is a very gradual tradeoff. Nowhere near "paramount".

Yes absolutely. Take games for example, bugs are absolutely tolerable and to be expected. In fact most software of any kind has known bugs that are simply accepted because the cost to fix them exceeds the value of doing so.

Any domain where the code will be used by a consumer who will go with a mostly correct program that has a fraction of the cost over one proven correct.

I suspect this to be the majority of code written.

>is there a domain where correctness is not paramount ?

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.

Yes, this is where this style of thinking leads to. Hard work is required so that we do not end up there. Can this race be won? I hope so.

Reply on news.ycombinator.com