14 ms·

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 prog

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.

auggierose 5y ago
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.
emodendroket 5y ago
Can't say we've really figured out proofs for program correctness now, can we?
- auggierose 5y ago
  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.
  - emodendroket 5y ago
    I admire your optimism.
  - IncRnd 5y ago
    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.
    - auggierose 5y ago
      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.
      - deleted 5y ago
        [deleted]
    - justanotherguy0 5y ago
      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
  - j16sdiz 5y ago
    Proofing correctness (in general) is incomputible (halting problem and stuffs). Those "prove" you see in academic paper are very specific case.
    - JadeNB 5y ago
      > 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.
    - ImprobableTruth 5y ago
      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.
    - Tainnor 5y ago
      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.
  - planb 5y ago
    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?
    - WanderPanda 5y ago
      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?
      - pbronez 5y ago
        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.
      - ImprobableTruth 5y ago
        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.
      - dgb23 5y ago
        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.
    - auggierose 5y ago
      Very good question! Try to figure it out yourself and you will see what is wrong with software development today.
rdedev 5y ago
All programming though ? That's a stretch. Like I'm pretty sure there are domains where correctness of programs is paramount
- worble 5y ago
  Is there a domain where correctness is not paramount?
  - carlhjerpe 5y ago
    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.
    - bamboozled 5y ago
      Yeah because losing money, market share or people’s data is fine ?
      - carlhjerpe 5y ago
        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.
  - MauranKilom 5y ago
    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".
SkyBelow 5y ago
>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.

auggierose 5y ago

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.

emodendroket 5y ago

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

auggierose 5y ago
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.
- emodendroket 5y ago
  I admire your optimism.
- IncRnd 5y ago
  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.
  - auggierose 5y ago
    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.
    - deleted 5y ago
      [deleted]
  - justanotherguy0 5y ago
    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
- j16sdiz 5y ago
  Proofing correctness (in general) is incomputible (halting problem and stuffs). Those "prove" you see in academic paper are very specific case.
  - JadeNB 5y ago
    > 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.
  - ImprobableTruth 5y ago
    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.
  - Tainnor 5y ago
    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.
- planb 5y ago
  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?
  - WanderPanda 5y ago
    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?
    - pbronez 5y ago
      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.
    - ImprobableTruth 5y ago
      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.
    - dgb23 5y ago
      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.
  - auggierose 5y ago
    Very good question! Try to figure it out yourself and you will see what is wrong with software development today.

rdedev 5y ago

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

worble 5y ago
Is there a domain where correctness is not paramount?
- carlhjerpe 5y ago
  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.
  - bamboozled 5y ago
    Yeah because losing money, market share or people’s data is fine ?
    - carlhjerpe 5y ago
      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.
- MauranKilom 5y ago
  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".

SkyBelow 5y ago

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