[racket] proof assistants, DrRacket and Bootstrap

On Sep 27, 2014, at 1:38 AM, Bill Richter wrote:

> Scheme is well-suited for writing a Scheme interpreter, because of the quote feature.  OCaml doesn't have a quote feature, so the question arises how to write an OCaml interpreter inside OCaml.  That's not quite what I want to do, but if anyone could explain how to do it, I'd be grateful.

Decouple parsing from interpreting and your ML interpreter for ML won't look too different from your Lisp/Racket/Scheme interpreter for Lisp/Racket/Scheme. Indeed, almost everyone who does the latter actually does some form of decoupling usually. 

In general, 

 (1) pick a representation for your chosen programming language that is tree-oriented, call it AST
 (2) pick a representation for the values that your programs may return, call it VAL 
 (3) design a function 

	interpreter : AST -> VAL 

 (4) for a typed language, also design a function 
	
	type_check : AST -> Boolean 

In ML, you might try

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


> I have a 7th grade student I'm trying to teach Racket, and I'm a bit confused about Bootstrap and Program By Design.  Is there any reason for my student not to just read HtDP?


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

2. HtDP is for college freshmen (roughly) and for high school students who have the patience to read. The occasional 7th and 8th grader work their way thru HtDP with adults who understand HtDP or learn to understand HtDP that way. The basic 7th grader will benefit from the material at bootstrap-world.org, which is what we use with many middle school students around the country. 

-- Matthias