[tpaschalis]

Second day in a row where HN frontpage features formally verified software!

If you're like me, and would like to get started, or just see what this is all about, the TLA+ homepage and video course (narrated by Leslie Lamport himself), is a nice resource [1].

In about half an hour you will have a brief understanding of what "formal specification languages" are, write and 'prove' your first small program/spec. If you have another hour to spend, keep the cheatsheet [2] near you and follow through, you will write and 'prove' more complex specs, plus you'll start thinking about systems in a more abstract way. Finishing up the video course you'll be able to start reading complex specs others have written, or write a spec for any algorithm you think is fun!

[1] https://lamport.azurewebsites.net/video/videos.html [2] https://lamport.azurewebsites.net/tla/summary-standalone.pdf

[drharby]

I really want this to be a sarcastic post demonstrating how thinly veiled some pr efforts are