Rigour is good for you and feasible
Michael Norrish, Peter Sewell, Keith Wansbrough · 2002
We summarise two projects that formalised complex real world systems: UDP and its sockets API, and the C programming language. We describe their goals and the techniques used in both. We conclude by discussing how such techniques might be applied to other system software and by describing the benefits this may bring.