News for hackers. Stuff that matters.

A comment on Using TLA+ to Understand Xen Vchan. Parent comment

Re:Using TLA+ to Understand Xen Vchan by mjb on Friday January 04, 2019 @11:43AM (#18825376)
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.

[ Parent | on HN ]
Re:Using TLA+ to Understand Xen Vchan by pron on Friday January 04, 2019 @11:49AM (#18825442)
There 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://drive.google.com/file/d/1rAn3N5hViv3xNe2E55lMzpFFym1...

[ Parent | on HN ]