Re: Layout syntax

Hans Aberg wrote:


> So when merely attempting to implement a proof checker for formal
> proofs written out in full that makes a correct use of
> metamathematics, there are a number of mathematical subtleties,
> which I do not think any system today handles. Surprise, surprise!


Interesting - I had been thinking that this kind of thing was long solved.


> -- But if somebody can give me a reference to a 100% correct proof
> checking system according to standard metamathematics, please let me
> know.


Coq? At least that's what's usually quoted at this point of the
discussion (but I don't know much about it myself).


> Then, if one by a proof means what humans usually write, then there
> is no clear distinction between a proof checker and a theorem prover,
> as the human written simplified proof merely invokes a proof search
> engine that is doing more work. The most extremely simplified proof
> is the empty one, which leads to the classical idea of a theorem
> prover. Also, the search engine will in any case be a modified Prolog
> type proof engine, so from the point of implementation, there is no
> clear distinction either.


At a minimum, the hand-written proof must include the sub-theorems of
all proofs by induction that are needed (and such a proof is required
for every loop and every recursion present, and the induction
information translates to loop invariants resp. assertions on the
recursive functions).
And, of course, the final theorems that one wants proven should be
written down :-)
These are the minimum requirements to make the task of giving a proof
decidable. Besides, explicitly writing down loop invariants will improve
code readability, so it's no loss if programmers have to write this down.
After that, constructing the proof is "just" worst-case exponential in
time and space... but there are a few theorems in Formal Logic that can
drastically cut down the search space.


> Also, not every theorem has a proof (by Goedel incompleteness), and
> there is no algorithm to tell which theorems have a proof.


It's my firm belief that all practically relevant theorems have
automatically detectable proofs.
There may be algorithms that are difficult to prove. However, these are
usually written with lots of explanations *how* the algorithm works -
which is an informal precursor to the full proof. Actually, the more
difficult algorithms are more rigorously proven, so I'd expect that
theorem provers will get more help for the more difficult software,
simply because humans need more help as well.
BTW when looking at the source code of a typical program, the required
"proofs" aren't much more than modus ponens, with the occasional
transformation of boolean expressions. That's no wonder: other
programming styles tend to be unmaintainable.


>> I meant checking that the theorem being proven is actually what we
>> want proven.
>
> The way you have worded this sentence, there is no way for a computer
> to tell if a theorem makes sense; only humans can do that.


Exactly.
The computer is *never* able to determine whether something makes sense
(read: is what we humans want).


My idea of theorem proving in connection with practical programming goes
like this:


1. The programmer writes a program.
2. The programmer wants to make sure that his program satisfies some
property. The exact nature of that property can vary: it might be a
statement on the program's results (or just a part of its results), or
on resource usage, or that it doesn't access certain resources, or
doesn't leak information - whatever the situation, it's the programmer
who decides which properties are interesting in the first place.
3. The programmer formalizes the properties, getting a theorem.
4. The theorem prover proves (or disproves) the theorem.


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.
But I think that it could be done, with current technology. Even if
there's no working theorem prover that correctly handles all current
metamathematics - we don't need to prove mathematical statements, we
want to prove statements about programs, at the level of formalization
that the relevant programming language has. We can even tell the theorem
prover to ignore the murky corners of the language definition ("assuming
that the following computation doesn't throw an exception, the result
will not be larger than twice the input" might be an theorem of that
kind - it's not as general as one would like, but it would be better
than nothing, right?)


>> For example, every tax calculation program is an existence proof
>> for a best way of filling out the tax forms given a set of input
>> parameters under the constraints of obeying the tax laws. This can
>> also be done in reverse: when I have a proof that such a solution
>> exists, without using the law of the excluded middle, then a
>> program that calculates the value can be automatically derived from
>> the proof.
>
> What you describe here is just a standard way to form a mathematical
> theory: One has as a basis certain axioms and rules of inference
> (essentially Prolog clause plus metamathematical typing), and proves
> from them some theorems. Then from axioms and theorems, one may want
> to prove new theorems.
>
> When one calculates a value, invokes a proved algorithm, or proves
> that two an implementation of an algorithm actually produces the
> results of the algorithm, those are just examples of theorems with
> proof. So, from the formal point of view, one does not get anything
> new here, even though it may be difficult to find good ways to
> implement practical systems.


Exactly my point.


> Eventually, I embarked onto the idea of attempting to implement a
> formally correct metamathematics. I use books on metamathematics by
> Elliott Mendelson, Stephen Cole Kleene, and Joseph R. Shoenfield. On
> that road I am right now.


This sounds interesting in its own right.


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

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