[racket] proof assistants, DrRacket and Bootstrap

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

Thanks, Matthias!  I know this is way off topic, but I think it's the sort of thing only Schemers understand, and I think HOL Light would be a lot better off my problem got solved.  There's a lot I didn't understand with your ML explanation.  Is this written down somewhere?  How to write a ML interpreter in ML using your type ideas?  Are you saying I don't need camlp parsing?  I would find that hard to believe.  Formal proofs in HOL Light are really just OCaml programs where a lot of code has already been evaluated.  Here's a simple Hilbert geometry program in my dialect:

let ExistsPointOffLine = theorem `;
  ∀l. Line l  ⇒  ∃Q. Q ∉ l

  proof
    intro_TAC ∀l, H1;
    consider A B C such that
    ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ ¬Collinear A B C     [Distinct] by fol I3;
    assume (A ∈ l) ∧ (B ∈ l) ∧ (C ∈ l)     [all_on] by fol ∉;
    Collinear A B C     [] by fol H1 - Collinear_DEF;
    fol - Distinct;
  qed;
`;;

I think I need the `;[...]` construct, which at present just turns my proof into a string without any backslash or newline problems, which is then passed to my function theorem.  The usual HOL Light style is like this, using instead a function prove: 

let MULT_0 = prove
 (`!m. m * 0 = 0`,
  INDUCT_TAC THEN ASM_REWRITE_TAC[MULT; ADD_CLAUSES]);;

Notice the related `[...]` construct, which I think sends the ordered pair off to heavy camlp parsing.  

Thanks for the 7th and 8th advice.  I think my student is smart and hard-working, and I (finally!) learned how to program reading your book HtDP, so it sounds like you're saying that I should be able to teach it to my student.  I went to bootstrap-world.org and, uh, maybe I didn't look hard enough, but I didn't find anything that looked juicy.  

-- 
Best,
Bill