# [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