[plt-scheme] on-execute method in drscheme:language:language<%>

On Jun 16, 2006, at 3:51 PM, Robby Findler wrote:

> You're advocating that the only way to run the theorem prover should 
> be when running inside drscheme and that it be impossible to avoid run 
> the theorem prover when you're in drscheme?

ACL2 is a programming system that intimately combines a language like 
Intermediate and a theorem prover. You can define functions only if 
they are provably [wrt to the given theorem prover] total. For example, 
length must terminate for all ACL2 values -- including non-lists -- and 
produce an answer (presumably an integer).

Master ACL2 splits this system into two pieces: a programming language 
and a theorem prover that you may want to run separately. The split is 
based on the idea that (1) students have HtDP-like training and (2) you 
design first (including testing) and prove later. [I believe that this 
is even possible in the original ACL2 environment but I could be 
mistaken.]

At OK U, Master ACL2 has worked great for the SE course in the spring.

Now at Bogota, someone is teaching students with much less tolerance 
for design discipline than the OKU students exhibited. In particular, 
they use Master ACL2 as a bad syntax for Scheme :-). What this means is 
that they write functions in a style for which it is impossible to 
prove termination or that may not even terminate on all inputs.

So we have been asked to change Master ACL2 so that every time you RUN 
the program, it first attempts to prove the termination property for 
all functions and then evaluates the definitions for use in the REPL. 
After rejecting the request at first, we have agreed to implement some 
version of it but combined with a preference for uncoupling the two 
processes.

-- Matthias