When I was a mere slip of a lad, formal methods became The Next Big Thing for a while, until we realised that users don’t actually know what they want so you can’t specify it and a sequence of events that led to Agile began.
Well, I was just ‘a little provocative’, argueing that “there is no point proving your code matches the spec if you haven’t understood the requirements” to someone who was probably right (on the Internet) and he sent me this: https://twitter.com/Hillelogram/status/971100796824801283.
I think it should be of interest to @auxbus and other mathemagicians. Don’t worry, I’ve already told him it looks like a job for Elixir. He dismisses functional purity as an option during the video.
I was surprised to hear the name Leslie Lamport mentioned in the video, who quite literally wrote the book on LaTeX and seems to have done most of the maintenance on the OMG standard for the last 30 years. I was unaware that he was also famous for algorithms and formal methods. There are 2 videos here that I haven’t watched yet but have interesting titles Events https://youtu.be/IFCVfeM9f5k and one on ‘ordering history’, which looks as if it may be the same.
From WikiP https://en.wikipedia.org/wiki/Leslie_Lamport
"Leslie Lamport was the winner of the 2013 Turing Award for imposing clear, well-defined coherence on the seemingly chaotic behavior of distributed computing systems, in which several autonomous computers communicate with each other by passing messages. He devised important algorithms and developed formal modeling and verification protocols that improve the quality of real distributed systems."