The Coq mailing list

[Ron <iampure AT gmail.com>]

2006/2/19, Lionel Elie Mamane 
<lionel AT mamane.lu>:
> On Sun, Feb 19, 2006 at 04:57:21PM +0100, Ron wrote:
>
> > Coq seems to be a well developed theorem prover, however, I read in
> > Chapter 1 of Coq'Art that Coq can't prove theorems about all
> > computable functions(in particular those that not terminate). So, it
> > seems I can't use Coq for my purposes, since I need to prove things
> > over programs that are possibly interactive, and hence don't need to
> > terminate.
>
> The "no programs that don't terminate" bit doesn't per se exclude
> interactive programs. Indeed, one usually want these program to
> respond sooner or later to every user input. So, one can see the whole
> program execution as a series of execution of smaller programs that
> each answer to _one_ input, give answer (and terminate).
>
> Besides, if your program doesn't terminate only when given infinite
> input (when the user keeps giving commands that are not "quit"), then
> it doesn't count as "not terminating" for this matter. What counts is
> "not terminating given a finite input".
>
> > More on the limitations of Coq. I have been taught that predicate
> > calculus can represent programs, so this would imply Coq can't do
> > this.
>
> Err... I'm not sure what you mean exactly. What is the relationship
> between the two claims you are making in that sentence alone?
In predicate logic you can state that a certain program, which will
never terminate, will never produce output FOO, and there exists
theorem provers which can handle predicate logic that can semi-decide
this. And Coq couldn't handle all computable functions (as in Chapter
1). So, if you can use Coq to do all of predicate logic, then there
must be something wrong in one of the above statements. They can not
be all correct at the same time modulo me ot understanding something.
And I want to prove things about the object language.

"Are you familiar with the large existing body of work on Foundational
Proof-Carrying Code?  In this area, we prove theorems about machine code
programs using no axioms but those of the machine architecture we run
on.  The most well-studied and -implemented theorems here are memory
safety theorems, which I think subsume buffer-overflow checking, given
the right definitions."
I have heard the term, yes. I have the book 'Advanced Topics in Types
and Programming Languages', which I think is related.

Now, it would be very interesting if someone would have formalized all
x86 instructions or similar. Did anyone do this? Or if not, what is
the most complex program of which non-trivial statements have been
proved? And what software is used most is this context? Coq? With what
libraries?

Thanks for all your answers,
   Ron