Re: TLA+ Video Course

It's not mathematics because what people want it to mean is that every variable other than small is unchanged, and there is no way to write a mathematical formula that asserts this. (Since there are infinitely many possible variables, such a formula would have to be infinitely long.) Of course you can design a language in which the statement has that meaning and give that language a precise mathematical semantics. But if that makes it math, then a C program is also math.

Leslie

On Monday, May 15, 2017 at 3:18:17 AM UTC-7, fl wrote:

The fourth video in the TLA+ Video Course has been released.

These are not criticisms, these are remarks I had in mind while I was listening to the video.

"It's not mathematics" : well the experience shows that in any mathematical texts many things are
left implicit. Not to mention the "intuitive" definition of continuity or limits in the XIXth texts,
the modern texts are full of missing information: for example mathematical texts use the phrase
"topological space" to mean either the structure
(so an ordered pair) or the base set (so the first element of the ordered pair). Likewise the
provisos are always missing. Likewise limit points in summations are often highly acrobatic.
Etc.

2) The fact that TLC solves the problem is purely fortuitous. It might be endless.

3) I like the idea that TLAPLUS can represent any digital system. Its ability to represent protocols
or standards and not only algorithms is usually not enough emphasized.

--
FL