Rustan Leino discusses with Carl and Richard the features and functionality of the Spec # programming language.