[tlaplus] Re: Draft of New TLA Book

[Peter Sovietov <peter.sovietov@xxxxxxxxx>]

Hi Leslie!

In the middle of the book (p. 146) you wrote:

"In the past 40 years, I have had essentially no contact with engineers who build real-time systems. I know of *only one case* in which TLA was used to check correctness of the design of a commercial real-time system [5]. From the point of view of our science, there is nothing special about real-time programs. However, how well tools work can depend on the application domain. The TLA+ tools were not developed with real-time programs in mind, and it’s unclear how useful they are in that domain."

But at the begining (p. 10) the reader can find the following text:

"Virtuoso was a real-time operating system. It controlled some instruments on the European Space Agency’s Rosetta spacecraft that explored a comet. Its creators decided to build the next version from scratch, starting with a high-level design written in TLA+. They described their experience in a book [47]."

As far as I understand, [5] and [47] are completely different works. Thus, in reality there are at least two known real-time projects related to TLA+,  or am I missing something?

среда, 3 января 2024 г. в 22:14:24 UTC+3, Leslie Lamport:

A draft of a new book I have tentatively titled A Science of Concurrent Programs is available here.  The book explains the scientific principles underlying the TLA+ language.  It contains a lot of math.  All the math beyond high school algebra is explained, but it will be tough going for readers who haven't taken an introductory university math class for computer science students that covers things like sets and logic.  The book contains little discussion of how TLA+ is used in practice, but it explains why TLA+ is what it is.

This is a preliminary version and I welcome comments, suggestions, and questions.  Anyone who is the first to report any error will be thanked in the final version. 

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7e866f9a-382d-4a5d-9818-b8e42dd420f9n%40googlegroups.com.