4 ms·

I feel like this needs to be repeated over and over. In theory, encryption and smart contracts and bitcoin are mathematically sound and "you can't argue with th

I feel like this needs to be repeated over and over. In theory, encryption and smart contracts and bitcoin are mathematically sound and "you can't argue with the math!" But the theory is written into real programs by humans, who make mistakes. The math is unassailable until, oops, it isn't, because someone forgot a bounds check!

traitormonkey 9y ago
..or the government had a bug placed in the random generator to weaken the crypto? In UK they want to do this openly now. What are you supposed to do roll your own crypto? Build your own CPU? It has code too - many operations are undocumented. We have this thing, the internet, where for the first time in history practically anyone can collaborate with anyone else in the world. We have the supposed bulwark of the right to bear arms and some rabidly protect it when in reality guns will be no use against a malign government. And yet often the same people are more than happy to relinquish this incredibly powerful weapon of liberty. Even worse some people are currently using this weapon to influence elections and seize power.
fmap 9y ago
Which is why you use mathematics to write formally verified software e.g. in Coq. :) This whole "move fast and break things" philosophy should be unacceptable, if you want people to trust in your new cryptocurrency/voting machine/etc, but try telling your investors that it'll take 5 years to develop the software instead of 5 weeks to "a first prototype" whose bugs and bad design decisions will haunt you forever...
- xfer 9y ago
  Coq extraction is not formally verified.
  - fmap 9y ago
    1) It will be very soon: http://www.cs.princeton.edu/~appel/certicoq/ http://www.cs.princeton.edu/~appel/certicoq/ CertiCoq is a formally verified compiler from Coq to assembly (using Compcerts backends), not just an extraction to Ocaml/Haskell/Scala. 2) Extraction is not the only approach to verifying software with Coq (see Verifiable C, or Bedrock). In other proof assistants, e.g., in Isabelle or HOL extraction isn't even available and so other approaches are common. For a nice example look at the bootstrapping process of CakeML (https://cakeml.org/ https://cakeml.org/). 3) Even if it wasn't, the point is that the trusted base with verified software is tiny compared to anything else that people are actually using. "It's not perfect" is not an excuse if it is basically perfect in practice. See the Csmith paper ("Finding and Understanding Bugs in C Compilers", https://embed.cs.utah.edu/csmith/ https://embed.cs.utah.edu/csmith/) and what they had to say about CompCert.

traitormonkey 9y ago

..or the government had a bug placed in the random generator to weaken the crypto? In UK they want to do this openly now. What are you supposed to do roll your own crypto? Build your own CPU? It has code too - many operations are undocumented. We have this thing, the internet, where for the first time in history practically anyone can collaborate with anyone else in the world. We have the supposed bulwark of the right to bear arms and some rabidly protect it when in reality guns will be no use against a malign government. And yet often the same people are more than happy to relinquish this incredibly powerful weapon of liberty. Even worse some people are currently using this weapon to influence elections and seize power.

fmap 9y ago

Which is why you use mathematics to write formally verified software e.g. in Coq. :) This whole "move fast and break things" philosophy should be unacceptable, if you want people to trust in your new cryptocurrency/voting machine/etc, but try telling your investors that it'll take 5 years to develop the software instead of 5 weeks to "a first prototype" whose bugs and bad design decisions will haunt you forever...

xfer 9y ago
Coq extraction is not formally verified.
- fmap 9y ago
  1) It will be very soon: http://www.cs.princeton.edu/~appel/certicoq/ http://www.cs.princeton.edu/~appel/certicoq/ CertiCoq is a formally verified compiler from Coq to assembly (using Compcerts backends), not just an extraction to Ocaml/Haskell/Scala. 2) Extraction is not the only approach to verifying software with Coq (see Verifiable C, or Bedrock). In other proof assistants, e.g., in Isabelle or HOL extraction isn't even available and so other approaches are common. For a nice example look at the bootstrapping process of CakeML (https://cakeml.org/ https://cakeml.org/). 3) Even if it wasn't, the point is that the trusted base with verified software is tiny compared to anything else that people are actually using. "It's not perfect" is not an excuse if it is basically perfect in practice. See the Csmith paper ("Finding and Understanding Bugs in C Compilers", https://embed.cs.utah.edu/csmith/ https://embed.cs.utah.edu/csmith/) and what they had to say about CompCert.