This past week, I was lucky enough to be able to attend the CyPhyAssure spring school, which featured talks by an impressive line-up of speakers covering everything from assuring autonomous robots for working with nuclear fusion reactors to modelling tools and techniques for hazard analysis of human-robot interactions (and everything in between). I was also fortunate to get an introduction to using the Isabelle proof assistant to write verified programs, and a crash course in using Isabelle/UTP, an implementation of Tony Hoare and He Jifeng's Unifying Theories of Programming in Isabelle, presented by one of the main driving forces behind the project Dr. Simon Foster.
All in all, I ended up in a world I'd never set foot in before (having more experience with Coq and working mainly in password security recently) and thoroughly enjoyed every second of it. The CyPhyAssure project will be running again, from what I hear, and it's well, well worth attending if you can.
A big thank you to all organisers, speakers and attendees for such a great experience, and paticularly to Simon for spearheading the project!