6 ms·
Admittedly I'm being a bit trollish as I say this, but do you get the same feeling from proofs that Pythagorean Theorem is correct? Proving things correct is m
by mabbo 5y ago
Admittedly I'm being a bit trollish as I say this, but do you get the same feeling from proofs that Pythagorean Theorem is correct?
Proving things correct is much harder than finding counter-examples that they aren't correct. But the methods do work. Their based on sound formal logic. Proofs can have mistakes, certainly, but it's a darn strong signal that their system is correct.
- tikhonj 5y agoThe problem with proving things about software is less in the proof itself and more in the connection between the proof and the real world. If somebody told me that they had a financial system whose security was based on applying the Pythagorean Theorem to physical triangles, it would raise exactly the same red flags—the theorem itself isn't a question, but it doesn't even try to capture how physical materials might be imperfect or change over time, and those are exactly the sort of inconsistencies a motivated attacker could exploit.
- klik99 5y agoI was going to reply but exactly this - I'll add that the proof work in the article is really interesting and I love to see practical work in formal proofs happening as a result of eth in particular. However 100% proven code on eth I just don't believe is 100% trustworthy. Another way of phrasing it is that the law of leaky abstractions means that though the code itself might be 100% correct, lower levels can puncture the assumptions and make that correctness moot - IE, unsinkable titanic vibes
- deleted 5y ago[deleted]