Using TLA+ to Understand Xen Vchan

Re:Using TLA+ to Understand Xen Vchan by pron on Friday January 04, 2019 @11:38AM (#18825310)

It may be worthwhile to allow declarations of the form

    VARIABLE x ∈ Nat

but I haven't considered all the implications of doing that. May be worth a discussion on the mailing list or at the conference in September.

As to "satisfying the type theory folks," I'm not sure what it means. Type theory studies the features of typed formalisms; it makes no claims as to when working in a typed formalism is preferable to working in untyped ones (although different people have different opinions). There are implementations of TLA in typed formalisms (in particular, Isabelle and Coq). Lamport explains why he designed TLA+ as an untyped language.

[ Parent | on HN ]

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 ]