3 ms·

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 th

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.

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.