1. 2

  2. 1

    I am super excited about this book. I believe formally verified software via proof assistants such as Coq represents the technology that will transition computer programming from an art to a true engineering discipline. Coq has been used for such things as producing a formally verified C compiler http://compcert.inria.fr/ . My favorite work in this area is Ur/Web http://www.impredicative.com/ur/ , a new web programming language that guarantees that web apps are invulnerable to many common web attacks.