[racket] proof assistants, DrRacket and Bootstrap

Matthias & Prabhakar, I think I see what you're saying now.  I need the camlp parser to turn my dialect-expressions into trees.  Then I turn my  tree into standard expressions just as one does in Scheme.  The only differences is that in Scheme we have the quote function that skips the parsing step.  So your ML code

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 | ...

looks a lot like the HOL Light definition of preterms: 

type preterm = Varp of string * pretype       (* Variable           - v      *)
             | Constp of string * pretype     (* Constant           - c      *)
             | Combp of preterm * preterm     (* Combination        - f x    *)
             | Absp of preterm * preterm      (* Lambda-abstraction - \x. t  *)
             | Typing of preterm * pretype;;  (* Type constraint    - t : ty *)

and so we can see one of these preterms in a standard term: 

# preterm_of_term `x + y`;;
val it : preterm =
  Combp
   (Combp
     (Constp ("+",
       Ptycon ("fun",
        [Ptycon ("num", []);
         Ptycon ("fun", [Ptycon ("num", []); Ptycon ("num", [])])])),
     Varp ("x", Ptycon ("num", []))),
   Varp ("y", Ptycon ("num", [])))

So the Scheme story works fine except that I haven't understood camlp or how HOL Light turns expressions `[...]` into preterms.  But I feel better about investing the time into learning camlp now that I see the Scheme story remains intact in HOL Light. And you're right  about my ignorance:

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

Right, there's something I seem not to have understood in either Scheme or ML, how when we create and evaluate our trees we retain the values of our variables.  I can figure that out, and HtDP sounds like a good place to start. 

PR> A Racketeer would probably tell you to use macros to define your
PR> dialect, instead of using an eval hack. The corresponding tool for
PR> OCaml is camlp4, and it sounds as if it would be worth your time
PR> to learn it thoroughly.

That's an interesting comparison, and since macros, maybe I can learn to like camlp.  In fact, maybe I ought to learn something about racket macros first. 

-- 
Best,
Bill