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