[Cryptography] one last thought for today on formal methods...

Perry E. Metzger perry at piermont.com
Mon Jun 9 09:33:04 EDT 2014


On Mon, 09 Jun 2014 11:00:38 +0100 ianG <iang at iang.org> wrote:
> > It would be a great shame if the good guys were not also using
> > [formal methods] across the board to close such holes.
> > 
> > I really encourage everyone to learn about the state of the art.
> 
> 
> What in practical managerial terms would be a recipe for achieving
> that? I mean in words like read this book/ do this masters/
> download this code...

If you're an individual programmer and not a manager, I do have
practical advice, which is learn how to use Coq, since it seems to be
(by far) the most important of the systems being used for such work
right now. seL4's proof was done in Isabelle/HOL but the
infrastructure associated with Coq appears to have most of the
momentum right now.

"Software Foundations" by Pierce et al is online for free, and is a
good very very basic introduction to Coq and some important related
ideas, "Certified Programming with Dependent Types" by Chlipala is
also online and is a much more advanced text.

As the area is still very young and under active development, there
is probably no substitute for reading lots of papers, especially
papers by people who have done work on proving real artifacts
correct.

I have no "practical recipe" suitable for managers. This is no
different from the situation one is faced with constantly when new
technologies get adopted: either get some of your best reports to
spend a bunch of time researching and learning, or hire someone to
teach your people, or hire some people who already have the needed
expertise.


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


More information about the cryptography mailing list