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 abou

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 https://lamport.azurewebsites.net/video/videos.html [2] https://lamport.azurewebsites.net/tla/summary-standalone.pdf https://lamport.azurewebsites.net/tla/summary-standalone.pdf