[Cryptography] Formal Verification

Perry E. Metzger perry at piermont.com
Tue Mar 22 08:31:11 EDT 2016


On Tue, 22 Mar 2016 05:49:20 -0000 dj at deadhat.com wrote:
> Formal verification of software is something I gave up hope on in
> 1991,

As did everyone else, including me, at that time. Again, the
technology has completely changed. It was de facto impossible back
then, and now it is something you can actually do.

The big change has been the development of systems like Coq where
dependent types and the Curry-Howard isomorphism are used to allow
proofs and programming to be done inside the same language and where
a combination of tactic based automation and human guidance are used
for the proofs themselves.

Again, for anyone who gave up on formal verification decades ago --
the world has changed. I would even go so far as to say that progress
is being made at an exceptionally rapid pace.

Perry
-- 
Perry E. Metzger		perry at piermont.com


More information about the cryptography mailing list