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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Fri, 4 Dec 2015 10:11:14 -0800 (PST)*References*: <dbc52c84-b6ce-4326-aeec-a7c17dd257c0@googlegroups.com> <33ED3621-4D95-4167-9232-9404968DD8E7@gmail.com> <02b4212f-9e09-4759-96a6-d73e7ae0881f@googlegroups.com> <708CF982-1782-422F-8445-6C87C4E7D8D6@gmail.com>

Here is my view, based on almost complete ignorance of the

mathematical foundations and a lot of practical experience using math.

I'm told that second-order logic is more powerful--for one reason,

because it can distinguish between standard and non-standard models of

the integers and first-order logic can't. I have never found this to

be a practical issue--even in pure math. I'm certainly not worried

about a bug occurring because an engineer implemented a non-standard

model of the integers.

mathematical foundations and a lot of practical experience using math.

I'm told that second-order logic is more powerful--for one reason,

because it can distinguish between standard and non-standard models of

the integers and first-order logic can't. I have never found this to

be a practical issue--even in pure math. I'm certainly not worried

about a bug occurring because an engineer implemented a non-standard

model of the integers.

I don't know Coq, but I'm sure that it's expressive enough

for all practical purposes. There's no good reason to write a set

like {1, {2,3}}, and making it impossible to write seems like a good

idea. However, I've found that there is no simple way to make it

impossible to write that set without also making it impossible to

write useful sets. As this implies, Coq is not simple. Chris

Newcombe will tell you that one can't expect an engineer to deal with

its complexity. That doesn't meant that there's anything wrong with

Coq; it just means that it's not meant for ordinary engineers. For

example, if you look at a math text, you might find that the symbol

+ is used in a single paragraph to mean several different things.

To formalize that math in TLA+, you'd have to use a different symbol

for each of those different meanings. That would drive a

mathematician crazy. Coq allows you to use the same symbol for all of

them. So, as George Gonthier will tell you, you need something like

Coq for formalizing serious math. Since system builders and algorithm

designers don't use that kind of math, they don't need to deal with

the complexity of a language like Coq.

for all practical purposes. There's no good reason to write a set

like {1, {2,3}}, and making it impossible to write seems like a good

idea. However, I've found that there is no simple way to make it

impossible to write that set without also making it impossible to

write useful sets. As this implies, Coq is not simple. Chris

Newcombe will tell you that one can't expect an engineer to deal with

its complexity. That doesn't meant that there's anything wrong with

Coq; it just means that it's not meant for ordinary engineers. For

example, if you look at a math text, you might find that the symbol

+ is used in a single paragraph to mean several different things.

To formalize that math in TLA+, you'd have to use a different symbol

for each of those different meanings. That would drive a

mathematician crazy. Coq allows you to use the same symbol for all of

them. So, as George Gonthier will tell you, you need something like

Coq for formalizing serious math. Since system builders and algorithm

designers don't use that kind of math, they don't need to deal with

the complexity of a language like Coq.

Leslie

**Follow-Ups**:**Re: [tlaplus] TLA+ logic***From:*Chris Newcombe

**References**:**TLA+ logic***From:*Ron Pressler

**Re: [tlaplus] TLA+ logic***From:*Stephan Merz

**Re: [tlaplus] TLA+ logic***From:*Ron Pressler

**Re: [tlaplus] TLA+ logic***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] TLA+ logic** - Next by Date:
**Re: [tlaplus] TLA+ logic** - Previous by thread:
**Re: [tlaplus] TLA+ logic** - Next by thread:
**Re: [tlaplus] TLA+ logic** - Index(es):