One of the oddest experiences of my professional career was attending a day long "training session" where Leslie Lamport tried to teach a team of engineers how

One of the oddest experiences of my professional career was attending a day long "training session" where Leslie Lamport tried to teach a team of engineers how to use TLA+ There was such a huge disconnect between the world views and educational backgrounds of a team of systems programmers and the world of formal proofs. All exacerbated by TLA+ using logic notation more common in Britain than America...