The "free online resource" I alluded to earlier is up on my Web page now.

I call it a "flânerie", but it's a mini-textbook on logic and proof 
assistants, using Racket to first construct a small proof assistant 
(Proust), expanding it to handle propositional and predicate logic, and 
then moving into discussion of the much larger Agda and Coq systems. --PR

On Monday, March 16, 2020 at 8:25:38 AM UTC-4, Adrian Manea wrote:
> Dear Prof. Ragde,
> Thank you very much for the reply! I watched your talk at the Racket con 
> more carefully today and noticed you specifically point out that you don't 
> give your students the whole code and that the entire project is presented 
> as a "proof of concept" and used especially for didactic purposes.
> I totally appreciate this approach and I have to say I don't feel quite 
> prepared to fill in the details myself. So I'm doing my best to learn some 
> preliminaries and general Racket first!
> Thank you,
> Adrian
> On Monday, March 16, 2020 at 12:08:51 PM UTC, Prabhakar Ragde wrote:
>> Hi! Sorry, I only get this list as a digest, so I didn't see your message 
>> until this morning. The code in the paper is not complete, and the paper 
>> isn't written so that a beginner in Racket could easily extract a working 
>> program from it. When I teach students this material, I give them a working 
>> starter file, and I will send that to you by private email, where we can 
>> also continue to discuss as needed.
>> I am at this moment working on converting my course materials on this 
>> topic into a free online resource similar to the one I did for functional 
>> data structures. But this is not ready yet. I hope to finish it in the next 
>> few months and I will post here when it is ready. --PR

You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
To view this discussion on the web visit

Reply via email to