The Coq mailing list

[G�rard Huet <Gerard.Huet AT inria.fr>]

Le mercredi 31 juillet 2002, à 09:49 PM, George Herson a écrit :

> Hi Gérard,
>
> That answers my main question, thank you.  I thought it was as you say, 
> but it seems strange to me that Turing Machines, as simple as they are, 
> can cover all computable problems yet there isn't an analogous coverage 
> of capability with formal method(s), even when used manually.
>
> Does there necessarily exist, for every constructable loop, a loop 
> invariant?

Your question begs the answer: yes, a loop ought to be constructable only
if the loop invariant exists.

Unfortunately, the answer is no, in general the invariant is not 
expressible
in the logic at hand. This is the cardinal failure of first-order logic.
In higher order logic of course you tell precisely which functions ought 
to
terminate and you get the principal invariant, which is a red herring 
anyway:
it is just the semantics of your program, specialised to the specific 
safety
invariant. If you know what your program does, you just write it down, 
and
that's enough.

I have put this answer to private mail on the coq-club mailing list since
this debate may be of interest to members of the Logical team or other 
users
of the Coq Proof Assistant. However, I know from experience with the 
Ocaml mailing list that it is counter productive to allow debates of a 
general nature on a hotline. There are forums, mailing lists, 
newsgroups, chats, whatever, which can relay debates of general nature 
such as motivations for such and such methodology or theory or practice.

But maybe such general interrogations ought to be distilled in a Coq 
FAQ ?

GH