Are there any research projects trying to make "proof" programs / languages?
Margaret Hamilton, of Apollo fame, designed and still advocates something called the Universal Systems Language: https://en.wikipedia.org/wiki/Universal_Systems_Language
How Did Software Get So Reliable Without Proof? (1996) [pdf]
61–70 of 126 posts
Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]
#62Earlier quoted context omitted.
Dependently typed languages may fit what you're asking for. See Idris and the book Type-Driven Development with Idris for an example of encoding critical information into the type system. Beyond that, see SPARK where you're limited to a provable subset of the Ada language (the subset has been extended with each version) so you can make assertions and it will attempt to prove (as part of compilation) that the assertio…
Combine Spark with Z as a specification language and you can get to "correct by construction". The only problem seems to be a reluctance to actually formulate a spec.
Yep. I've tried to use Z Notation in the past but haven't had much luck (doesn't help that I had no collaborators so was learning on my own). I've often, also, worked on projects that had decent (but massive and all prose) specs. They would've benefited by formalizing at least portions of them.
I'm not sure I'd try to use Z Notation at this point, given that there are other systems out there that seem to fill the same niche but with better tooling. Event-B and TLA+ are the two I've explored the most.
Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]
#63Earlier quoted context omitted.
It is also replacing humans most of the time as well, who are prone to making all sorts of errors. Worse, humans can make the same error twice even after being corrected.
Software can also make the same mistake, thousands of times per second or more :)
"same" is the operative word. Easier to correct the same mistake every time than a different mistake on unpredictable executions.
Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]
#64Because reliable and proof are not the same concepts and one is not needed for the other. Proof is logical certainty for all time ( in the past, present and future ). Reliability is not. Reliability doesn't require mathematical proof - this goes for airplanes to your kitchen faucet to software. Software became more and more reliable through testing, errors, fixes/patches, etc. Also, many times good enough is good eno…
The control systems for airplanes often have a significant number of mathematical proofs.
Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]
#65Because reliable and proof are not the same concepts and one is not needed for the other. Proof is logical certainty for all time ( in the past, present and future ). Reliability is not. Reliability doesn't require mathematical proof - this goes for airplanes to your kitchen faucet to software. Software became more and more reliable through testing, errors, fixes/patches, etc. Also, many times good enough is good eno…
The control systems for airplanes often have a significant number of mathematical proofs.
Sure because the alternative is death
Me shit posting is not a life or death situation so a bug here or there is fine
Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]
#66Because reliable and proof are not the same concepts and one is not needed for the other. Proof is logical certainty for all time ( in the past, present and future ). Reliability is not. Reliability doesn't require mathematical proof - this goes for airplanes to your kitchen faucet to software. Software became more and more reliable through testing, errors, fixes/patches, etc. Also, many times good enough is good eno…
A proof is only performed under certain assumptions and is far from a logical certainty for all time.
Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]
#67The first sentence of the article begins "Twenty years ago", and yet the article itself is undated. This appears to be entirely normal for scientific papers. Can anyone tell me how this foolishness came to be considered acceptable among scientists, and why it persists?
This was published in 1996, where the journal was dated.
https://link.springer.com/chapter/10.1007/3-540-60973-3_77
Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]
#68Because reliable and proof are not the same concepts and one is not needed for the other. Proof is logical certainty for all time ( in the past, present and future ). Reliability is not. Reliability doesn't require mathematical proof - this goes for airplanes to your kitchen faucet to software. Software became more and more reliable through testing, errors, fixes/patches, etc. Also, many times good enough is good eno…
The control systems for airplanes often have a significant number of mathematical proofs.
The bolts don't, and yet they don't (usually) fail.
Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]
#69Are there any research projects trying to make "proof" programs / languages?
Re: How Did Software Get So Reliable Without Proof? (1996) [pdf]
#70lol, tell that functional programming proponents. They will tell you that current software is basically crap and they can't understand how the majority tolerates this state of affairs.
This is common misconception of students or perhaps research people, who don't need to actually earn money with their projects.
Software needs to be as reliable as it needs to be to satisfy customers and not erode customer trust. And that's it.
Now sure, you can proof everything mathematically and ship your fitbit application within 10 years instead of 10 days, but there are more than a few problems with this approach:
1. You will be bankrupt before you even proved the first theorem
1. Your proofs will turn out to not align with realities of a real world environment
1. Hardware has bugs
1. Software you depend on has bugs
1. Requirements change like a flag in the wind, i.e. 100 times faster than you can prove your little theorems
1. Customers don't give a shit if your fitbit app is never crashing and always does what you think it should do. Especially if its 10 years outdated and doesn't do what customers want lol.