[racket] proof assistants, DrRacket and Bootstrap

Matthias, I'm still thrilled with your advice about writing a ML interpreter in ML, but I think what you told me doesn't suffice, and in particular:

MF> 1. HtDP explains the above in a couple of sections. 

I think HtDP only does part of the job.  I think there is nothing about Scheme evaluators past Section 17.7, where you extend the 14.4 evaluator to functions:
HtDP> The goal of this section is to extend the evaluator of section
HtDP> 14.4 so that it can cope with function applications and function
HtDP> definitions.
In the Section 14.4 evaluator you don't even have variables:
http://htdp.org/2003-09-26/Book/curriculum-Z-H-19.html#node_sec_14.4
I'm sure HtDP is fine for a first course, and I profited from reading it again, but I think a better job is done in the OCaml manual, in Sec 1.7 of 
http://caml.inria.fr/pub/docs/manual-ocaml/coreexamples.html
where they have something a lot like your 

MF>   type ast = VAR of String | LAM of String * ast | APP of ast * ast | CONST of int | ADD of ast * ast 
MF>   type val = BASIC of int | FUNCTION of val -> val | ...

But what I don't like is the OCaml manual's 

Om> We first define a function to evaluate an expression given an
Om> environment that maps variable names to their values. For
Om> simplicity, the environment is represented as an association list.

That's fine, as long as the Scheme/ML program we're evaluating is self contained, because the only variables will be the ones we define in our program.  But what if the program has free variables which are already defined?  How do we get our trees to use the values in a Scheme environment already defined?  I am sure you racketeers know the answer, and maybe it would be a good exercise to put in your second edition:
http://www.ccs.neu.edu/home/matthias/HtDP2e/
All I can guess is that is Sec 17.7, you say that a 
HtDP> the function's name [and] the parameter name [are] symbols
so probably all variables are represented in the tree as symbols, and I guess we need a function that will take these symbols and return their values given in the bigger environment.  

-- 
Best,
Bill