<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Wed, Mar 16, 2016 at 7:00 PM, Perry E. Metzger <span dir="ltr"><<a href="mailto:perry@piermont.com" target="_blank">perry@piermont.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">Two decades ago you couldn't have dreamed of writing a verified<br>
program of any significant size, and now we have worked examples of<br>
quite large formally verified artifact, including compilers, large<br>
chunks of microprocessors, a microkernel, etc. etc.</blockquote><div><br></div><div>With verifiable computation, you don't need to check the whole program either, only verify the result:</div><div><br></div><div><a href="https://pbs.twimg.com/media/Cd8BwlIUsAAMgQP.jpg">https://pbs.twimg.com/media/Cd8BwlIUsAAMgQP.jpg</a><br></div><div><br></div><div><img src="cid:ii_1539252da5ac1524" alt="Inline image 1" width="510" height="480"><br></div><div> </div></div>-- <br><div class="gmail_signature">Tony Arcieri<br></div>
</div></div>