3 ms·

One thing that sets software apart from other engineering disciplines is that they are grounded in physics (bits running on a semiconductor doesn't matter for t

One thing that sets software apart from other engineering disciplines is that they are grounded in physics (bits running on a semiconductor doesn't matter for this discussion) and have been around (in some form) for thousands of years. How do we know if a design is sound? We can check it by doing the math. How do we know if a program is sound (what does that even mean? There's our first problem)? Well, we rely on a large compendium of heuristics that are based on nothing but experiences compiled over the past ~60 years. Also, that compendium is constantly being added to. Also, virtually everyone disagrees on what should/shouldn't be in this compendium.

just_steve_h 6y ago
I'm wading into waters that are way over my head here, but my understanding is that it is possible for software to be provably correct, in the mathematical sense of "proof." I'm well aware of the admixture of folklore, experience, and caffeine-fueled inspiration that constitutes much of the software that runs our world.
- ghaff 6y ago
  There's work going on in formal verification but it has many limitations. I'd also point out that in MechE/CivE fields, you're still dependent on materials (and maintenance) working as advertised. It's also often the case that operating conditions just end up being different from what was designed for or certain failure modes weren't considered. See, e.g. the Citibank Building in NYC http://www.slate.com/blogs/the_eye/2014/04/17/the_citicorp_tower_design_flaw_that_could_have_wiped_out_the_skyscraper.html http://www.slate.com/blogs/the_eye/2014/04/17/the_citicorp_t...
- vvanders 6y ago
  Have a peek a metastability[1], any time a digital system crosses a clock domain there's basically statistics making sure the whole thing doesn't fall over. From need a better MTBF? Throw a couple more inline flip-flops. [1] https://en.m.wikipedia.org/wiki/Metastability_(electronics) https://en.m.wikipedia.org/wiki/Metastability_(electronics)
- Dirlewanger 6y ago
  I think being able to prove that a program can be correct is getting close to P=NP territory.
  - Raptor22 6y ago
    It's very difficult but there have been strides in that direction: http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4....
  - aklein 6y ago
    Cannot prove some program is correct, in general, because that’s effectively the halting problem. But in practice it is sufficient to enforce (prove) the absence of behaviors via constraints like types or contracts.
- bluGill 6y ago
  You can, but first we need to figure out what correct is in the first place. I can prove hello world doesn't overflow buffers, but it is a bit harder to prove that my font renders the letters vs some random scribbles.
- rocqua 6y ago
  It is possible to prove software adheres to a certain specification. This is time consuming, and how feasible it is depends a lot on how your specification was written. It generally also depends on how your software was written. The big issue is that writing a useful specification can be hard. Especially if you want to also make the specification easy to check. A side issue is that your proof will make assumptions about how a computer works that are simplified.
- archi42 6y ago
  Source: I work on static analyzers, so I'm biased to that. We can not prove everything, as others pointed out the fundamental issue here is the "halting problem". However, this doesn't mean we can't prove anything. Wikipedia says: > In computability theory, Rice's theorem states that all non-trivial, semantic properties of programs are undecidable. I often feel like the "trick" is to push the trivial stuff to be as useful as possible. You can work from several vectors: 1. You build better static analyzers (difficult and computationally expensive the further you push it - but that's what we're doing) 2. reduce the complexity of the "analyzed thing" (high level language, assembly,...) to allow for easier analysis, while still being useful (a assembly language only supporting 'nop' is trivial to analyze, but pretty useless overall; otoh you can disallow some constructs in C to make the language easier to analyze). There are of course other forms of "provably correct". E.g. programming in a language that has proofs attached to it, like coq [which is the name of a proof assistant]. Disclaimer: I've never used coq myself, but know plenty who do. I think that's something that might interest you. [And thanks to the genius who christened that tool: No, seriously, I'm not trying to be rude!] [edit] Didn't check that link, but maybe you find it interesting https://www.cs.princeton.edu/courses/archive/spring13/cos510/sf/Basics.html https://www.cs.princeton.edu/courses/archive/spring13/cos510... There are of course other approaches than coq, e.g. Isabelle is often mentioned. See the "See also" on https://en.wikipedia.org/wiki/Coq https://en.wikipedia.org/wiki/Coq

just_steve_h 6y ago

I'm wading into waters that are way over my head here, but my understanding is that it is possible for software to be provably correct, in the mathematical sense of "proof." I'm well aware of the admixture of folklore, experience, and caffeine-fueled inspiration that constitutes much of the software that runs our world.

ghaff 6y ago
There's work going on in formal verification but it has many limitations. I'd also point out that in MechE/CivE fields, you're still dependent on materials (and maintenance) working as advertised. It's also often the case that operating conditions just end up being different from what was designed for or certain failure modes weren't considered. See, e.g. the Citibank Building in NYC http://www.slate.com/blogs/the_eye/2014/04/17/the_citicorp_tower_design_flaw_that_could_have_wiped_out_the_skyscraper.html http://www.slate.com/blogs/the_eye/2014/04/17/the_citicorp_t...
vvanders 6y ago
Have a peek a metastability[1], any time a digital system crosses a clock domain there's basically statistics making sure the whole thing doesn't fall over. From need a better MTBF? Throw a couple more inline flip-flops. [1] https://en.m.wikipedia.org/wiki/Metastability_(electronics) https://en.m.wikipedia.org/wiki/Metastability_(electronics)
Dirlewanger 6y ago
I think being able to prove that a program can be correct is getting close to P=NP territory.
- Raptor22 6y ago
  It's very difficult but there have been strides in that direction: http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4....
- aklein 6y ago
  Cannot prove some program is correct, in general, because that’s effectively the halting problem. But in practice it is sufficient to enforce (prove) the absence of behaviors via constraints like types or contracts.
bluGill 6y ago
You can, but first we need to figure out what correct is in the first place. I can prove hello world doesn't overflow buffers, but it is a bit harder to prove that my font renders the letters vs some random scribbles.
rocqua 6y ago
It is possible to prove software adheres to a certain specification. This is time consuming, and how feasible it is depends a lot on how your specification was written. It generally also depends on how your software was written. The big issue is that writing a useful specification can be hard. Especially if you want to also make the specification easy to check. A side issue is that your proof will make assumptions about how a computer works that are simplified.
archi42 6y ago
Source: I work on static analyzers, so I'm biased to that. We can not prove everything, as others pointed out the fundamental issue here is the "halting problem". However, this doesn't mean we can't prove anything. Wikipedia says: > In computability theory, Rice's theorem states that all non-trivial, semantic properties of programs are undecidable. I often feel like the "trick" is to push the trivial stuff to be as useful as possible. You can work from several vectors: 1. You build better static analyzers (difficult and computationally expensive the further you push it - but that's what we're doing) 2. reduce the complexity of the "analyzed thing" (high level language, assembly,...) to allow for easier analysis, while still being useful (a assembly language only supporting 'nop' is trivial to analyze, but pretty useless overall; otoh you can disallow some constructs in C to make the language easier to analyze). There are of course other forms of "provably correct". E.g. programming in a language that has proofs attached to it, like coq [which is the name of a proof assistant]. Disclaimer: I've never used coq myself, but know plenty who do. I think that's something that might interest you. [And thanks to the genius who christened that tool: No, seriously, I'm not trying to be rude!] [edit] Didn't check that link, but maybe you find it interesting https://www.cs.princeton.edu/courses/archive/spring13/cos510/sf/Basics.html https://www.cs.princeton.edu/courses/archive/spring13/cos510... There are of course other approaches than coq, e.g. Isabelle is often mentioned. See the "See also" on https://en.wikipedia.org/wiki/Coq https://en.wikipedia.org/wiki/Coq