This is perhaps tangential, but my flânerie "Logic and Computation Intertwined" uses Racket as its implementation language. Students learn about propositional and predicate logic by using Racket to construct a small proof assistant based on intuitionistic type theory, and then using that to solve their homework problems. I use it in a second-year undergraduate course.
I've added a new chapter on interaction (filling holes in incomplete proofs via successive refinement), which is already covered in the earlier chapter for propositional logic, but which gets complicated for predicate logic due to dependencies. The chapter brings in some advanced Racket features, and new concepts such as unification. I don't know of another tutorial introduction to these ideas below advanced graduate level. Perhaps some of you will find it interesting or useful.
https://cs.uwaterloo.ca/~plragde/flaneries/LACI/index.html
7 Likes
This has been on my reading list for a while. Probably time to speed through it in preparation for POPL'22!
1 Like
I'm a big fan of this work. I was going to ask if you had any thoughts about Lean, but a quick look at
https://artagnon.com/articles/leancoq
leads me to believe that Lean might not be a great fit for this material.
Thanks again for building this, I enjoyed LACI immensely.
1 Like
I'm keeping an eye on Lean, but yes, they've made some choices I don't care for, the language seems to change often, and I was quite underwhelmed by the workshop I attended at a major conference.
By the way, @jbclements, since I know that you're interested in music and sound, you might be amused by this.
https://cs.uwaterloo.ca/~plragde/flaneries/FIMS/index.html
2 Likes
Cool! That sounds like something @jeapostrophe would be into, as well. Seems related to this: https://dl.acm.org/doi/abs/10.1145/2975980.2975981
5 Likes