5 ms·

I agree with the other commenter about the comma in this sentence. But I'd also like to point out that 100% error-free code is possible. There's a whole branch

I agree with the other commenter about the comma in this sentence. But I'd also like to point out that 100% error-free code is possible. There's a whole branch of computer science dedicated to it: formal verification. I personally have used Coq to write certified code in the past, and I'm quite confident that my code was 100% error-free. Of course, there are some qualifications one should make regarding such a claim: you have to trust that your specification is "correct", that your hardware is functioning correctly, that the proof checker didn't accept a bogus proof, that the underlying logic (e.g., the calculus of inductive constructions) is consistent, etc. That's a lot of things to trust, but the point is that you don't have to trust yourself.

whatshisface 6y ago
I really can't trust myself to write a specification. I know this because I have written errors in tests before - even when all I'm doing is trying to work out some properties that the answer ought to have, I can still make a mistake. It's just usually less likely that I would make a mistake, because the specification is simpler than the algorithm. So, it is not really fair to downplay the chance that you could have a wrong specification, although it would be equally wrong to use that as an excuse to downplay the value of Coq.
- rrobukef 6y ago
  WPA2 is a formally verified protocol. It lasted 14 years: https://www.krackattacks.com/ https://www.krackattacks.com/. Now it's partially formally verified.
  - danielscrubs 6y ago
    You can't prove that something is secure, because to be applicable in mathematics/computer science there has to exist a precise definition. If someone is just saying "This is a formally verified protocol" without what they actually checked for, they are salespeople not mathematicians. "The authors of the KRA paper were able to understand what the proofs were about, and why they don’t cover the KRACK vulnerability. Even though the original proofs didn’t reveal security flaws, a principled approach would use these proofs in order to discover where to look." https://galois.com/blog/2017/10/formal-methods-krack-vulnerability/ https://galois.com/blog/2017/10/formal-methods-krack-vulnera...

whatshisface 6y ago

I really can't trust myself to write a specification. I know this because I have written errors in tests before - even when all I'm doing is trying to work out some properties that the answer ought to have, I can still make a mistake. It's just usually less likely that I would make a mistake, because the specification is simpler than the algorithm. So, it is not really fair to downplay the chance that you could have a wrong specification, although it would be equally wrong to use that as an excuse to downplay the value of Coq.

rrobukef 6y ago
WPA2 is a formally verified protocol. It lasted 14 years: https://www.krackattacks.com/ https://www.krackattacks.com/. Now it's partially formally verified.
- danielscrubs 6y ago
  You can't prove that something is secure, because to be applicable in mathematics/computer science there has to exist a precise definition. If someone is just saying "This is a formally verified protocol" without what they actually checked for, they are salespeople not mathematicians. "The authors of the KRA paper were able to understand what the proofs were about, and why they don’t cover the KRACK vulnerability. Even though the original proofs didn’t reveal security flaws, a principled approach would use these proofs in order to discover where to look." https://galois.com/blog/2017/10/formal-methods-krack-vulnerability/ https://galois.com/blog/2017/10/formal-methods-krack-vulnera...