"Provably secure" is BS. "Provably secure against attacks X, Y, Z" is achievable, and a good thing to have.https://twitter.com/galois/status/921064905763147776 …
-
-
What tools do you use?
-
Coq, Idris, FStar.
-
but all this tools do not link atifacts to the specification, right? they are „just“ another interpretation of the specification?
-
No. They work directly on the implementation.
-
I think the formal verification has to be created on the requirement level and then must applied on code or model …(1/2)
-
Not if you use a dependently typed language.
End of conversation
New conversation -
-
-
Also: people should read the stated assumptions and actual claims.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
The best way to become a humble programmer is to try to prove even the most simple properties you think your code has.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.