[racket] users Digest, Vol 109, Issue 63

Please take me off the list

Thanks

On Sat, Sep 27, 2014 at 12:00 PM,  <users-request at racket-lang.org> wrote:
> Send users mailing list submissions to
>         users at racket-lang.org
>
> To subscribe or unsubscribe via the World Wide Web, visit
>         http://lists.racket-lang.org/users/listinfo
> or, via email, send a message with subject or body 'help' to
>         users-request at racket-lang.org
>
> You can reach the person managing the list at
>         users-owner at racket-lang.org
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of users digest..."
>
>
> [Racket Users list:
>  http://lists.racket-lang.org/users ]
>
>
> Today's Topics:
>
>    1.  proof assistants, DrRacket and Bootstrap (Prabhakar Ragde)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Sat, 27 Sep 2014 10:33:15 -0400
> From: Prabhakar Ragde <plragde at uwaterloo.ca>
> To: "users at racket-lang.org" <users at racket-lang.org>
> Subject: [racket]  proof assistants, DrRacket and Bootstrap
> Message-ID: <5426CAAB.2010400 at uwaterloo.ca>
> Content-Type: text/plain; charset=ISO-8859-1; format=flowed
>
>> I have a few questions that might be off-topic.  Are you interested
>> in formal proofs?  Have you considered adapting DrRacket to give an
>> integrated editor for a proof assistant?  The proof assistants Coq
>> and Isabelle use jedit and ProofGeneral, which I think aren't nearly
>> as nice as DrRacket.  I actually use HOL Light, which nobody uses an
>> integrated editor for.  Here are the slides for a talk I gave at the
>> Institut Henri Poincar? in the workshop ``Formalization of
>> mathematics in proof assistants''
>> http://www.math.northwestern.edu/~richter/RichterIHPslide.pdf
>
> 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. I know something like this is possible, because at
> Brown they used DrRacket to prepare and run OCaml programs, a few years
> ago. I really don't have the time to work on this, though. (And if I
> did, I would first work on teaching language subsets of Haskell, which I
> also would like to have inside DrRacket.)
>
>> HOL Light and Coq are written in OCaml, a dialect of ML, which is
>> therefore similar to Scheme, but it has one difference that I wonder
>> if anyone here's knows how to deal with.  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.
>
> In my senior undergraduate programming language course, I have them
> write various interpreters and typecheckers in various languages,
> including Racket, OCaml, and Haskell. In the latter two, you need to use
> algebraic datatypes to build an abstract syntax tree, and interpret
> that. So the expression (* (+ 1 2) (- 3 4)) might become
>
> (Mult (Plus (Num 1) (Num 2)) (Minus (Num 3) (Num 4)))
>
> Writing an interpreter for such an AST is even easier than in
> Racket/Scheme, due to concise pattern-matching syntax. But parsing an
> expression written in faux OCaml/Haskell is quite complicated. I don't
> ask students to do that, since it really is part of a separate course
> (both languages come with general parsing tools that can be used).
> Parsing is much easier in Racket/Scheme because of the similarity of
> code/data and the presence of 'read'.
>
>> 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?
>
> You should view word from the authors/developers as definitive, but I
> would say that if your student has good algebraic skills, then using
> HtDP/2e is the right path. If not, Bootstrap may be a way to help
> develop those skills. --PR
>
>
> End of users Digest, Vol 109, Issue 63
> **************************************