Re: Layout syntax

Hans Aberg wrote:
> [...]


I think we've been talking a bit at cross-purpose here:
* You are interested in doing pure mathematics.
* I am interested in proving the properties of programs, with as much
automation as possible and reasonable.


My claims should read in conjunction with my objective; I'm well aware
that they are overgeneral if you want to do general math. This
particularly applies to


>> It's my firm belief that all practically relevant theorems have
>> automatically detectable proofs.


The main issue here is that, for my objectives, all practically
relevant theorems are those based on a given program. That's a
tremendous amount of information that a theorem prover can use, since
the program structure already reflects the proof structure. Also, all
properties of a program can be proven using constructive
mathematics. This also eases the task of the prover tremendously.


Any theorem prover that's intended for checking (or even finding)
valid theorems in general mathematics has a far harder job: it cannot
restrict itself to constructive mathematics, and it doesn't have a
program. My goals are far more modest than yours :-)


>> Of course, details may vary wildly. The theorems could be set up
>> before the first line of code is written. The programmer might have
>> to state lemmas to help the theorem prover along. The theorem
>> prover would have to be quite smart about reporting errors, since
>> just a "the property doesn't hold" response isn't going to be very
>> helpful. Etc. etc.
>
> Actually, I have a very simple system: One writes the math, axioms,
> theorems, proofs, etc., in a file. Then one runs the program, and if
> all is syntactically correct, it writes an output file with the same
> math, but indicating the statements whose proofs failed. One can get
> further diagnostics in a log file, the deductions of selected math
> portions, etc. This way, it is usually easy to capture errors.


This would probably be a good approach for error reporting in a program
property prover as well.


I'm not sure that this is enough though. If the
programmer/mathematician expects the prover to get along from one
theorem to the next without the programmer's help, and the prover
doesn't, this may mean one of two things: Either the prover is too
dumb, or the programmer/mathematician made a mistake. I'm not sure
what strategies would help the programmer/mathematician to find out
which situation holds, and how to remedy the situation in the fastest
possible way.


For programmers, the error may even be in the theorems he wants to
prove (i.e. he stated a theorem that's more general than is needed,
and that actually doesn't hold). I'm not sure how common such a
situation might be for a mathematician (I could imagine that similar
situations could occur when the mathematician sets up a lemma, but I'm
not sure how far this is relevant - the work of a mathematician is far
more open-ended than that of a programmer).


Regards,
Jo
--
Currently looking for a new job.

Return to the comp.compilers page.
Search the comp.compilers archives again.