While we see the many visible roles computers play in our lives every day, through laptops, phones,  search engines, and the internet, computers also play an even more critical invisiblerole.  They prevent the brakes on our cars from locking up when we brake too hard, they fly our airplanes through dense air traffic and around large storms, they manage our electrical and water systems, and (for some people) even control the beating of their hearts.  When you build a bridge you can analyze it through a series of equations to understand the maximum weight it can take, but unfortunately, even after nearly 70 years of computing, it remains incredibly difficult to build computer systems that we can say anything mathematical about.  With this new support from the National Science Foundation, Professor Sherwood and his students and collaborators are seeking to transform the way in which these critical computer systems are designed and analyzed.  

To achieve this vision of more robust computer controlled systems we need new approaches to creating them that includes both the hardware and the software together.  Traditional computer hardware is really built for speed and efficiency at all costs, but often times we have more than enough speed and efficiency to get a job done.  Instead we need systems that, while remaining quite efficient, also are far easier to understand and reason about mathematically.  Building on top of powerful theories of computation (such as lambda-calculus) a new computer system where every action it takes corresponds directly to a nice set of equations can be created.  Rather than try and solve the resulting math equations by hand, this project reconsiders the way computer processors are designed from the ground up so that they work in perfect harmony with state-of-the-art computer-automated mathematical theorem provers.   To demonstrate that this approach is actually useful on real world problems the investigators are building a completely new computer system around this approach with all of the hardware design, computer languages, and operating system-like software needed.