[racket-users] Re: Understanding P. Ragde's Proust

Thank you very much for coming back and posting this resource! I will be reading it carefully and I'm already sure there is a lot of useful content! Much appreciated. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this gro

[racket-users] Re: Understanding P. Ragde's Proust

The "free online resource" I alluded to earlier is up on my Web page now. https://cs.uwaterloo.ca/~plragde/flaneries/LACI/ 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 pro

[racket-users] Re: Understanding P. Ragde's Proust

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 didact

[racket-users] Re: Understanding P. Ragde's Proust

On Sunday, March 15, 2020 at 10:00:59 AM UTC-4, Adrian Manea wrote: > > > I'm a mathematician delving into type theory and proof assistants and with > special interests in Racket. > > I'm now trying to understand and implement P. Ragde's Proust > "nano proof a