3 ms·
Gotta love TLA+ I wonder if anyone has worked on porting it to Lean and making tactics for it
by vatsachak 4mo ago
Gotta love TLA+
I wonder if anyone has worked on porting it to Lean and making tactics for it
- uptodatenews 4mo agoYou run into Rices theorem if you try to apply it too heavily. I made https://github.com/RCSnyder/tlaplus-process-studio https://github.com/RCSnyder/tlaplus-process-studio https://tlaplus-process-studio.com/ https://tlaplus-process-studio.com/ For local only high level modelling. Its not a full tie into the actual model checker, but its meant to serve as a first step into system modelling for state machine modelling for beginners
- another_twist 4mo agoi am not sure if a lean port is important. TLA+ could do with a bit more TLC (pun intended) with regards its devEx. Also congratulations to the author, I'll try and reproduce this over the weekend.