3 ms·
Unfortunately the benefit of TLA+ is the act of modeling your system painstakingly. The actual checker helps confirm your hypothesis, etc. But skipping the mode
by leoqa 4mo ago
Unfortunately the benefit of TLA+ is the act of modeling your system painstakingly. The actual checker helps confirm your hypothesis, etc. But skipping the modeling and outsourcing it is not ideal. I’ve always struggled reasoning about models my team mates wrote, and will often have to mentally go through the process of arriving at the same abstractions/invariants etc before I can understand it.
- UltraSane 4mo agoExactly. I view a complete TLA+ specification as a kind of metalanguage that can be used with LLMs to generate code from.
- goostavos 4mo agoAgreed. To quote Leslie Lamport, "the hardest part of TLA+ is learning to think abstractly." There's always a moment, usually annoyingly late in the process, where I realize I've been massively overthinking everything or solving the wrong problem. Time is an essential an ingredient. Clear thinking is extremely hard. LLMs are definitely useful along the way, but the thinking is the spiritually fulfilling part.