[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Mon, 15 May 2017 03:29:50 -0700 (PDT)*References*: <b19fb379-6a8c-4241-ada3-673038ea76db@googlegroups.com> <6c4305b5-1584-4321-9c24-8aaca6a3c13a@googlegroups.com> <1af9e47d-fc86-4709-8ec2-6abbaeb828d4@googlegroups.com>

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 areleft 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 theprovisos 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 protocolsor standards and not only algorithms is usually not enough emphasized.--FL

**Follow-Ups**:**Re: TLA+ Video Course***From:*fl

**References**:**TLA+ Video Course***From:*Leslie Lamport

**Re: TLA+ Video Course***From:*Leslie Lamport

**Re: TLA+ Video Course***From:*fl

- Prev by Date:
**Re: TLA+ Video Course** - Next by Date:
**Re: TLA+ Video Course** - Previous by thread:
**Re: TLA+ Video Course** - Next by thread:
**Re: TLA+ Video Course** - Index(es):