[racket] proof assistants, DrRacket and Bootstrap

On 2014-09-28, 12:57 AM, Bill Richter wrote:

> I'm making a dialect of HOL Light with different syntax by
> interpreting one of my programs as a string and then breaking the
> string up into the component pieces, but then I need this
> Toploop/exec hack to evaluate my variables.  That sounds like the
> Scheme eval, and in Scheme you can solve that problem nicely with the
> quote feature.

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