On Mon, Sep 07, 2015 at 12:07:14PM +0000, Alfonso De Gregorio wrote:
Comments in [0] suggest "formal verification".
The only hope to have a formal verification that extends also to algebraic properties, is to start from formal specifications. A top-down approach in stark contrast with the dynamic, agile, and pragmatic "ship, then test" paradigm [1] and the "don't worry, be crappy" mantra [2], repeated by entrepreneurs innovating the most.
We need better security trade-offs.
Re "formal verification". I am skidiot at formal verification (FW). So far my best achievement in FW is "Axiom free proof of False" in Coq (is it Cock?). I did this by native code execution via plugins in Coq (the plugins were part of the "pr00f"), which in theory can falsify other proofs depending on the file permissions. Much letter I learned that the lovely micro$oft heavily depend on plugins in their Cock "pr00fs" and accidentally something broke the check of the "pr00f" for result of significant importance (something like "coqchk") due to some fault in the plugin and/or Coq. The p00f failure was discussed on academic site. In short, I consider Coq a charlatan tool, and likely security vulnerability, since a proof can easily execute native code. Let me know if you need further references. btw, doesn't your post contradict another post of yours here: https://cpunks.org/pipermail/cypherpunks/2015-September/009032.html
While I sympathize with your point of view, and while I would welcome a full equivalence of implementations, ...