4 ms·

Most proofs have assumptions about the system which can be (occasionally/rarely) violated, but which make the proof tractable, or simply don't model features of

Most proofs have assumptions about the system which can be (occasionally/rarely) violated, but which make the proof tractable, or simply don't model features of the real system. I think the point is that you can have a proof of correctness in a crypto package that doesnt account for power-usage side-channel attacks, for example. This is true, but beside the point: a library with no proofs about it doesn't solve that problem, and the library with proofs tells me I don't have certain problems for sure. The question is then: is it worth the proof development effort to only get those partial guarantees? I would argue yes, for a lot of reasons (and high EAL levels tend to agree that it is for high-assurance stuff), but it's a matter of some debate.

KirinDave 10y ago
I am fairly sure, upon reading this thread, that this is not zzzcpan's point. His point is to denigrate the entire practice if providing proofs. I think he's referring to fields which, given their critical and highly difficult nature, should in fact start with the proofs and work to invalidate the system over increasingly more total domains of implemention. You're right that you can take a mathematical proof out of the realm of abstract math and it's new domain may not have all the guarantees we need, but this means we need to extend the system to account for the new domain (and within this domain, the proof is not valid). But the poster doubled down on this idea that "there are constraints proofs ignore" within the existing domain. Outside of convenient proofs that upper division students provide, this is not true. A good example of this process and the nature of "pure" CS interacting with the real world is the field of distributed databases. As the field has grown, proofs are expected to aggressively model real world conditions and in fact go further, modeling outright adversarial conditions unlikely to occur in the real world.
- SomeStupidPoint 10y ago
  Oh, that's quite possible. I was merely reiterating a common (and I think sensible) point that we can't write proofs about things we don't have the computational resources to address or just plain don't realize are an issue. Both are very real challenges to using proofs about our software, and should be kept in mind when talking about the field. The said, Im a proponent of everything from proofs about abstract algorithm properties to basic model checking on a spec to using formal methods to extract a program with guaranteed propertied from a formal spec we've written proofs about in something like Coq. DARPA funding HoTT research should clue anyone in that this stuff is useful.
  - KirinDave 10y ago
    I think we should work to prove software and that's an ongoing process, but it's hard to imagine using an algorithm without a proof of at least correctness and convergence. I just see people talking about domains and saying, "We don't need proofs for software" like they learned literally nothing from OpenSSL last year. And perhaps they did not, but I think we all should recognize that the stakes are getting pretty high and it's time to stop pretending we're all supervillan-level software designers.

KirinDave 10y ago

I am fairly sure, upon reading this thread, that this is not zzzcpan's point. His point is to denigrate the entire practice if providing proofs. I think he's referring to fields which, given their critical and highly difficult nature, should in fact start with the proofs and work to invalidate the system over increasingly more total domains of implemention. You're right that you can take a mathematical proof out of the realm of abstract math and it's new domain may not have all the guarantees we need, but this means we need to extend the system to account for the new domain (and within this domain, the proof is not valid). But the poster doubled down on this idea that "there are constraints proofs ignore" within the existing domain. Outside of convenient proofs that upper division students provide, this is not true. A good example of this process and the nature of "pure" CS interacting with the real world is the field of distributed databases. As the field has grown, proofs are expected to aggressively model real world conditions and in fact go further, modeling outright adversarial conditions unlikely to occur in the real world.

SomeStupidPoint 10y ago
Oh, that's quite possible. I was merely reiterating a common (and I think sensible) point that we can't write proofs about things we don't have the computational resources to address or just plain don't realize are an issue. Both are very real challenges to using proofs about our software, and should be kept in mind when talking about the field. The said, Im a proponent of everything from proofs about abstract algorithm properties to basic model checking on a spec to using formal methods to extract a program with guaranteed propertied from a formal spec we've written proofs about in something like Coq. DARPA funding HoTT research should clue anyone in that this stuff is useful.
- KirinDave 10y ago
  I think we should work to prove software and that's an ongoing process, but it's hard to imagine using an algorithm without a proof of at least correctness and convergence. I just see people talking about domains and saying, "We don't need proofs for software" like they learned literally nothing from OpenSSL last year. And perhaps they did not, but I think we all should recognize that the stakes are getting pretty high and it's time to stop pretending we're all supervillan-level software designers.