DeepSpec Summer School 2017 – a summary

I have spent the last two and a half week in Philadelphia attending the first DeepSpec Summer School, In this post I want to summarize the event and give an overview of all the courses.

The DeepSpec Project is a research project lead by several US East Coast universities (University of Pennsylvania, MIT, Yale University and Princeton University) and aims to “push forward the state of the art in applying computer proof assistants to verify realistic software and hardware stacks at scale”. It consists of several smaller projects, including a formal verification of a hypervisor (CertiKOS), LLVM (Vellvm), Coq compiler (CertiCoq) and GHC’s Core language (CoreSpec).

The goal of DeepSpec Summer School was to introduce people to real-life formal verification using Coq proof assistant. School was divided into three parts. All the lectures can be found on a YouTube channel. Coq code for the courses is available on GitHub. Summer school’s web page also provides installation instructions as well as other supplementary material (click on a given lecture or select from “Lectures” tab).

Week 0: Coq Intensive

First three days of the summer school were a very intensive introductory course on Coq lead by Benjamin Pierce. This essentially covered the first volume of Software Foundations. (Aside: For those of you who don’t know yet, original Software Foundations online book has been split into two volumes: Logical Foundations and Programming Language Foundations. Also, a third volume has been added to the series: Verified Functional Algorithms by Andrew Appel. All three volumes can be found here, although expect that this link will likely become broken soon when this draft versions become an official release. There are also plans for two more volumes, one on Separation Logic and another one on Systems Verification.)

Week 1: Programming Language Verification

First full week of the school consisted of four courses centred around programming language verification:

  • Property-based random testing with QuickChick by Benjamin Pierce. I assume many of you heard about Haskell library called QuickCheck. It offers property-based testing: programmer writes properties that the should hold for a given piece of code and QuickCheck tests whether they hold for randomly generated test data. QuickChick is implementation of the same idea in Coq. Now, you might wonder what is the point of doing such a thing in Coq. After all, Coq is about formally proving that a given property is always true, not randomly testing whether it holds. I was sceptical about this as well, but it actually turns to be quite a good idea. The point is, specifications are difficult to write and often even more difficult to prove. They are especially difficult to prove when they are false ;-) And this is exactly when QuickChick can be beneficial: by trying to find a counter-example for which a stated property does not hold. This can indeed save programmer from spending hours on trying to prove something that is false. If QuickChick doesn’t find a counter-example we can start writing a formal proof.
    This course also gives a nice overview of type classes in Coq.
  • The structure of verified compiler by Xavier Leroy. This series of lectures was based on CompCert, which is a formally verified C compiler. The ideas behind formal verification of a compiler were presented on a compiler of Imp (a toy imperative language used in Software Foundations) to a simple virtual machine. Fourth, final lecture covered the CompCert project itself. To me this was the most interesting course of the summer school.
  • Language specification and variable binding by Stephanie Weirich. Software Foundations is a great book, but it completely omits one topic that is very important in formalizing programming languages: dealing with variable bindings. In this courses Stephanie presented “locally nameless” representation of variable bindings. This is something I had planned to learn for a very long time but couldn’t find the time.
  • Vellvm: Verifying the LLVM by Steve Zdancewic. For a change, in this course Imp was compiled to a simplified variant of LLVM, the compilation process being verified of course. Also, a nice introduction to LLVM.

Week 2: Systems Verification

Courses during the second week put more focus on verifying computer systems. Again, there were four courses:

  • Certifying software with crashes by Frans Kaashoek and Nickolai Zeldovich. The topic of this course was certification of a hard-drive operating routines, including bad-sector remapping and a simple virtual RAID 1 implementation. Although still using toy examples, specifications presented during this course were much more abstract giving a good idea how to scale to a real-world system verification. I found this course very difficult to follow, although the lectures were really superb. Note: materials for this one course are available in a separate GitHub repo.
  • CertiKOS: Certified kit operating systems by Zhong Shao. Ok, I admit I was completely unable to follow this series of lectures. Way to difficult. In fact, I skipped two out of four lectures because I figured out it will make more sense to work on homework assignments for other lectures.
  • Program-specific proof automation by Adam Chlipala. Unsurprisingly to those who know Adam’s “Certified Programming with Dependent Types” book, his course focused on proof automation using Ltac. One lecture was specifically dedicated to proofs by reflection.
  • Verified Functional Algorithms by Andrew Appel. This course covered a majority of third volume of new Software Foundations.

Summary

First and foremost let me say this: DeepSpec Summer School was the best research meeting I have ever attended. The courses were really good and inspiring, but the most important thing that made this summer school so great were fantastic people who attended it. Spending evening hours together working on homework assignments was especially enjoyable.

There might be a 2018 edition of the summer school so be on the lookout – this is a really great event for anyone interested in Coq and formal verification.

Moving to University of Edinburgh

I wanted to let you all know that after working for 8 years as a Lecturer at the Institute of Information Technology (Lodz University of Technology, Poland), I have received a sabbatical leave to focus solely on research. Yesterday I began my work as a Research Associate at the Laboratory for Foundations of Computer Science, University of Edinburgh. This is a two-year post-doc position. I will be part of the team working on the Skye project under supervision of James Cheney. This means that from now on I will mostly focus on developing the Links programming language.

First impression of “Real World OCaml”

Tomorrow I will be flying to Cambridge to attend International Summer School on Metaprogramming. One of the prerequisites required from the participants is basic knowledge of OCaml, roughly the first nine chapters of “Real World OCaml” (RWO for short). I finished reading them several days ago and thought I will share my impressions about the book.

rwoRWO was written by Yaron Minsky, Anil Madhavapeddy and Jason Hickey. It is one of a handful of books on OCaml. Other titles out there are “OCaml from the Very Beginning” and “More OCaml: Algorithms, Methods and Diversions” by John Whitington and “Practical OCaml” by Joshua Smith. I decided to go with RWO because when I asked “what is the best book on OCaml” on #ocaml IRC channel RWO was an unanimous response from several users. The title itself is obviously piggybacking on an earlier “Real World Haskell” released in the same series by O’Reilly, which was in general a good book (though it had its flaws).

The first nine chapters comprise about 40% of the book (190 pages out of 470 total) and cover the basics of OCaml: various data types (lists, records, variants), error handling, imperative programming (eg. mutable variables and data structures, I/O) and basics of the module system. Chapters 10 through 12 present advanced features of the module system and introduce object-oriented aspects of OCaml. Language ecosystem (ie. tools and libraries) is discussed in chapters 13 through 18. The remaining chapters 19 through 23 go into details of OCaml compiler like garbage collector or Foreign Function Interface.

When I think back about reading “Real World Haskell” I recall that quite a lot of space was dedicated to explaining in detail various basic functional programming concepts. “Real World OCaml” is much more dense. It approaches teaching OCaml just as if it was another programming language, without making big deal of functional programming model. I am much more experienced now than when reading RWH four years ago and this is exactly what I wanted. I wonder however how will this approach work for people new to functional programming. It reminds my of my early days as a functional programmer. I began learning Scala having previously learned Scheme and Erlang (both unusual for functional languages in lacking a type system). Both Scala and OCaml are not pure functional languages: they allow free mixing of functional and imperative (side-effecting) code. They also support object-oriented programming. My plan in learning Scala was to learn functional programming and I quickly realized that I was failing. Scala simply offered too many back-doors that allowed escaping into the imperative world. So instead of forcing me to learn a new way of thinking it allowed me to do things the old way. OCaml seems to be exactly the same in this regard and RWO offers beginners little guidance to thinking functionally. Instead, it gives them a full arsenal of imperative features early on in the book. I am not entirely convinced that this approach will work well for people new to FP.

“Real World OCaml” was published less than three years ago so it is a fairly recent book. Quite surprisingly then several sections have already gone out of date. The code does not work with the latest version of OCaml compiler and requires non-obvious changes to work. (You can of course solve the problem by working with the old version of OCaml compiler.) I was told on IRC that the authors are already working on the second edition of the book to bring it to date with today’s OCaml implementation.

Given all the above my verdict on “Real World OCaml” is that it is a really good book about OCaml itself (despite being slightly outdated) but not necessarily the best book on basics of functional programming.

Staypressed theme by Themocracy