4 ms·
I think it is worth a discussion. I simply meant that adding simple macros wouldn't make TLA+ typed, and so wouldn't make the people who think TLA+ should be t
by mjb 8y ago
I think it is worth a discussion.
I simply meant that adding simple macros wouldn't make TLA+ typed, and so wouldn't make the people who think TLA+ should be typed any happier than they are today.
- pron 8y agoThere are typed TLA formalisms[1], but they're not called TLA+. I don't know what it means to want TLA+ to be typed. It's like saying someone wants the untyped lambda calculus to be typed. I can understand someone who thinks Lamport was misguided in designing TLA+ as an untyped formalism, but so far it seems that he was right (for the reasons I detailed in my Reddit comment). [1]: https://www.isa-afp.org/entries/TLA.html https://www.isa-afp.org/entries/TLA.html, https://drive.google.com/file/d/1rAn3N5hViv3xNe2E55lMzpFFym1lpx9C/view https://drive.google.com/file/d/1rAn3N5hViv3xNe2E55lMzpFFym1...