Re: Heartbleed

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Sat, 12 Apr 2014 21:15:17 +0200, Pascal J. Bourguignon  
<pjb@informatimago.com> a écrit:
> There will always be bugs remaining, even in tested and more
> importantly, **even in proven software!**

Are you really sure? Can you point to at least one example please (except  
bad specifications)? Unless there is a soundness issue (some checker has  
this issue, and are known to has one, but the most famous ones don't) or  
else a specification error, I really can't see how. Note a specification  
error will fail with a dynamic language too: a dynamic language will do  
the wrong thing if you tell it to do the wrong thing, it won't guess and  
fix it‑self on your behalf. So, the only remaining possible case of  
“broken formally verified software” which is relevant here, is the one  
with a formal verifier which has soundness issues (possibly the so called  
Pollack-inconsistency, which is a human/formal‑system interface issue).  
Still note you can check a proof with different systems, and there are  
standard appearing to help in that matter. Ex. OpenTheory, a standard to  
import/export HOL proofs in a raw format, not human readable, but fully  
machine checkable. If the proof of a theory is checked with say, two or  
three different enough systems, it's very unlikely there is a issue with  
the proof.


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University