I've been learning TLA+ for the past two months, hoping I could use it as a formal language for software design generally and not just for concurrent systems. I'm enamored with the idea of using math formalisms to describe a state machine.<p>But now that I've gone through Lamport's (very charming) video tutorials at OP's link and studied some of the specifications at<p><a href="https://github.com/tlaplus/Examples/tree/master/specifications" rel="nofollow">https://github.com/tlaplus/Examples/tree/master/specificatio...</a><p>I'm less sure now that I can. I'll keep plugging away, but if anyone here has any suggestions or offers any alternatives, I'm all ears.
Raymond Hettinger just have a talk at PyCon an hour ago about formal reasoning and solvers. There’s a lot of polish in the talk, with a whole ReadTheDocs site with runnable Python code with solvers written from scratch. The slides aren’t out yet publicly or privately, but I would highly recommend going through the examples when the PyCon committee releases the information. The way he puts it makes it much less intimidating than I thought it would be.<p>Also Raymond is a very nice guy :D
One thing that bothered me while trying to learn the TLA+ is the two different but equivalent forms or syntax for writing it: a mathematical formula/expression form and code/program form. This topic is difficult as it, and having to deal with not one but two equivalent forms of saying one thing is perhaps a bit hard on a learner. I wish if there was a tutorial of TLA+ that ditched the whole mathematical formula notation, and taught only the code form.
Interesting. I've worked concurrent systems in VHDL and Verilog (but not SystemVerilog) stacks, and those using C, C++, Haskell, OCaml, Ruby, Go, Erlang and Rust.<p>I wonder if this approach could formally verify systems like seL4.<p>Here's an approach to verifying concurrent systems using coq:<p><a href="https://www.sciencedirect.com/science/article/pii/S1571066108000765" rel="nofollow">https://www.sciencedirect.com/science/article/pii/S157106610...</a>