[racket] proof assistants, DrRacket and Bootstrap

On 2014-09-27, 5:50 PM, Bill Richter wrote:
> Thanks, Prabhakar, this is exactly what I wanted, and you know something about it (I was barely able to install Coq):

I struggled with installing it also, especially since I'm using a Mac. 
Racket has spoiled us in that respect.

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

I don't have enough practice in OCaml to grasp what your code does (and, 
yes, it is way off-topic), but I do know that about once every month or 
two, someone posts to this list about using 'eval' in Racket, and they 
are warned not to use it unless they really know what they are doing and 
have a suitable application (which is rare). That warning probably is 
doubled in a statically-typed language, in which 'eval' should not even 
be possible without subverting the type system (I gather this is what 
you are doing). Translating the gist of suggestions to such posters, I 
would say: do you really need to execute *any* expression? If not, use 
OCamllex and/or OCamlyacc (maybe Menhir, or a smaller and cleaner parser 
combinator library) to write a parser for your language subset, and then 
write an interpreter for the resulting ASTs. --PR