[Cryptography] Formal Verification (was Re: Trust & randomness in computer systems)

[Tony Arcieri]

On Wed, Mar 16, 2016 at 7:00 PM, Perry E. Metzger <perry at piermont.com>
wrote:

> Two decades ago you couldn't have dreamed of writing a verified
> program of any significant size, and now we have worked examples of
> quite large formally verified artifact, including compilers, large
> chunks of microprocessors, a microkernel, etc. etc.


With verifiable computation, you don't need to check the whole program
either, only verify the result:

https://pbs.twimg.com/media/Cd8BwlIUsAAMgQP.jpg

[image: Inline image 1]

-- 
Tony Arcieri
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.metzdowd.com/pipermail/cryptography/attachments/20160319/1edd97d3/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: image.png
Type: image/png
Size: 558658 bytes
Desc: not available
URL: <http://www.metzdowd.com/pipermail/cryptography/attachments/20160319/1edd97d3/attachment-0001.png>