[racket] proof assistants, DrRacket and Bootstrap

Thanks, Prabhakar, this is exactly what I wanted, and you know something about it (I was barely able to install Coq):

   I am teaching a grad course using Coq right now, and using Proof
   General within Emacs for it. That is not bad, but I would love to
   have a DrRacket interface.

   > OCaml doesn't have a quote feature, so the question arises how to
   > write an OCaml interpreter inside OCaml.  

   In my senior undergraduate programming language course, I have them
   write various interpreters and typecheckers in various languages,
   including Racket, OCaml, and Haskell. 
   [...]

I know this is way off-topic, but it seems to me that Schemers are the only people who want an elegant solution here: 

   But parsing an expression written in faux OCaml/Haskell is quite
   complicated. [...] Parsing is much easier in Racket/Scheme because
   of the similarity of code/data and the presence of 'read'.

I think it's a parsing question I'm stuck on.  I think I need to use camlp to avoid the following hack/kludge which I learned from the HOL Light experts, found in my file 
hol_light/RichterHilbertAxiomGeometry/readable.ml
which is part of the HOL Light distribution:

(* From update_database.ml: Execute any OCaml expression given as a string.  *)

let exec = ignore o Toploop.execute_phrase false Format.std_formatter
  o !Toploop.parse_toplevel_phrase o Lexing.from_string;;

(* Following miz3.ml, exec_thm returns the theorem representing a string, so *)
(* exec_thm "FORALL_PAIR_THM";; returns                                      *)
(* val it : thm = |- !P. (!p. P p) <=> (!p1 p2. P (p1,p2))                   *)

let thm_ref = ref TRUTH;;

let exec_thm s =
  if Str.string_match (Str.regexp "[^;]*;") s 0 then raise Noparse
  else
    try exec ("thm_ref := (("^ s ^"): thm);;");
      !thm_ref
    with _ -> raise Noparse;;

When I posted my question on the OCaml list, the experts said don't ever use Obj.magic, but I think they didn't think much of me using Toploop either.

-- 
Best,
Bill