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.
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.
Leslie