If you suspend your transcription on amara.org, please add a timestamp below to indicate how far you progressed! This will help others to resume your work!
Please do not press “publish” on amara.org to save your progress, use “save draft” instead. Only press “publish” when you're done with quality control.
<p>Today's developers of computer software and hardware are tremendously effective, compared to their predecessors. We have found very effective ways of <b>modularizing</b> and <b>validating</b> our work. The talk is about ammunition for these activities from a perhaps-unexpected source.</p>
<p><b>Modularity</b> involves breaking a complex system into a hierarchy of simpler pieces, which may be written and understood separately. Structured programming (e.g., using loops and conditionals instead of <tt>goto</tt>s) helps us read and understand parts of a single function in isolation, and data abstraction lets us encapsulate important functionality in objects, with guarantees that other code can only access the private data by calling public methods. That way, we can convince ourselves that the encapsulated code upholds certain essential properties, <i>regardless of which other code it is linked with</i>. Systematic unit testing also helps enforce contracts for units of modularity. Each of these techniques can be rerun automatically, to catch regressions in evolving systems, and catch those regressions in a way that accurately points the finger of responsibility to particular modules.</p>
<p><b>Validation</b> is an important part of development that encompasses testing, debugging, code review, and anything else that we do to raise our confidence that the system behaves as intended. Experienced engineers know that validation tends to take up the majority of engineering effort. Often that effort involves mentally taxing activities that would not otherwise come up in coding. One example is thinking about test-case coverage, and another is including instrumentation that produces traces to consult during debugging.</p>
<p>It is not hard for working developers to imagine great productivity gains from better ways to break systems into pieces or raise our confidence in those pieces. The claim I will make in this talk is that a key source of such insights has been neglected: <b>machine-checked mathematical proofs</b>. Here the basic functionality is an ASCII language for defining mathematical objects, stating theorems about them, and giving proofs of theorems. Crucially, an algorithm checks that purported proofs really do establish the theorems. By going about these activities in the style of programming, we inherit usual supporting tools like IDEs, version control, continuous integration, and automated build processes. But how could so esoteric a task as math proofs call for that kind of tooling, and what does it have to do with building real computer systems?</p>
<p>I will explain a shared vision to that end, developed along with many other members of my research community. Let me try to convince you that all of the following goals are attainable in the next 10 years.</p>
<ul>
<li>We will have complete computer systems implementing moderately complex network servers for popular protocols, <i>proved to implement those protocols correctly, from the level of digital circuits on up</i>. We will remove all deployed code (hardware or software) from the trusted computing base, shifting our trust to much smaller specifications and proof checkers.</li>
<li>Hobbyists will be able to design new embedded computing platforms by mixing and matching open-source hardware and software components, also mixing and matching <i>the proofs</i> of these components, <i>guaranteeing no bugs at the digital-abstraction level or higher</i>, with <i>no need for debugging</i>.</li>
<li>New styles of library design will be enabled by the chance to attach a <i>formal behavioral specification</i> to each library. For instance, rank-and-file programmers will able to assemble their own code for cryptographic protocols, with code that looks like reference implementations in Python, but <i>getting performance comparable to what experts handcraft in assembly today</i>. Yet that benefit would come with <i>no need to trust that library authors have avoided bugs or intentional backdoors</i>, perhaps even including <i>automatic proofs of cryptographic security properties</i>.</li>
</ul>
<p>Main technical topics to cover to explain my optimism:</p>
<ul>
<li>The basic functionality of <i>proof assistants</i> and why we should trust their conclusions</li>
<li>How to think about system decomposition with specifications and proofs, including why, for most components, we do not need to worry about specification mistakes</li>
<li>The different modes of applying proof technology to check or generate components</li>
<li>The engineering techniques behind cost-effective proof authoring for realistic systems</li>
<li>A hardware case study: <a href="https://github.com/mit-plv/kami">Kami</a>, supporting component-based digital hardware authoring with proofs</li>
<li>A software case study: <a href="https://github.com/mit-plv/fiat-crypto">Fiat Cryptography</a>, supporting correct-by-construction auto-generation of fast code for elliptic-curve cryptography</li>
<li>Pointers to where to look next, if you would like to learn more about this technology</li>
</ul>