first push on paper content.  focusing on ripping out features piecewise and relating making correct-by-construction arguments along the way.