getting a formal education

• Mail folder: QED
• Next message: Konrad Slind: "Cold water"
• Previous message: Zdzislaw Meglicki: "Re: Cold water"

From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: qed@mcs.anl.gov
Subject: getting a formal education
Message-id: <93Apr30.022254met_dst.8088@sunbroy14.informatik.tu-muenchen.de>
Date: 	Fri, 30 Apr 1993 02:22:50 +0200
Sender: qed-owner
Precedence: bulk

I agree with John Harrison and Josh Guttman: students seem like a good
initial target for a QED-like project. For one thing, their requirements
are certainly more well-understood (and uniform!) than those of working
mathematicians: students need to pass their courses. To do that they
have to understand the material in the course. The material has already
been defined by others: all we formal methodistas need to do is provide
that material, making sure that it is consistent and accurate (which is
our stock in trade after all). We can provide it for free and it can be
everywhere, thanks to things like the internet.

Josh writes:

> And that means that systems should be very serious about issues such
> the ability to take large ("human-sized") proof steps and having a
> style of formalization and proof that is very close to the ethos of
> traditional rigorous mathematics.

Yes. To echo a message from Victor Yodaiken, the formal presentation of
a classic text at the original author's level would be a milestone well
worth working towards. I would suggest staying in the realm of computer
science, and look forward to a "Hopcroft and Ullman Made Formal"
appearing soon at an ftp site near me.

I guess there might be a legal problem too - would this violate
copyright?


The formalization of such a course raises a couple of problems:

1. Rules of inference too powerful. 

Could it be the case that one wants the student to get practice in
proving theorems by a certain method, but the automatic or pervasive
methods of the proof system solve the goals in one step? 


2. Opacity of rules.

At a difficult point in a proof the student may want to examine the
proof in ever-increasing detail. Theorem proving systems that provide a
few "heavyweight" decision procedures as their basic rules seem not to
be amenable to such decomposition.


Konrad.