# New chapter in "Logic and Computation Intertwined" **URL:** \ **Category:** Show & Tell\ **Created:** [December 3, 2021, 3:33pm UTC](https://racket.discourse.group/t/new-chapter-in-logic-and-computation-intertwined/338 "2021-12-03T15:33:12Z")\ **Posts on this page:** 6\ **Page:** 1
**Author:** ![plragde](https://avatars.discourse-cdn.com/v4/letter/p/ac8455/32.png) [@plragde](https://racket.discourse.group/u/plragde)\ **Post date:** [December 3, 2021, 3:33pm UTC](https://racket.discourse.group/t/new-chapter-in-logic-and-computation-intertwined/338/1 "2021-12-03T15:33:12Z")
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](https://cs.uwaterloo.ca/~plragde/flaneries/LACI/index.html) ---
**Author:** ![benknoble](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/benknoble/32/16_2.png) [@benknoble](https://racket.discourse.group/u/benknoble)\ **Post date:** [December 3, 2021, 5:08pm UTC](https://racket.discourse.group/t/new-chapter-in-logic-and-computation-intertwined/338/2 "2021-12-03T17:08:47Z")
This has been on my reading list for a while. Probably time to speed through it in preparation for POPL'22! ---
**Author:** ![jbclements](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/jbclements/32/11_2.png) [@jbclements](https://racket.discourse.group/u/jbclements)\ **Post date:** [December 3, 2021, 6:04pm UTC](https://racket.discourse.group/t/new-chapter-in-logic-and-computation-intertwined/338/3 "2021-12-03T18:04:44Z")
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](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. ---
**Author:** ![plragde](https://avatars.discourse-cdn.com/v4/letter/p/ac8455/32.png) [@plragde](https://racket.discourse.group/u/plragde)\ **Post date:** [December 3, 2021, 6:23pm UTC](https://racket.discourse.group/t/new-chapter-in-logic-and-computation-intertwined/338/4 "2021-12-03T18:23:24Z")
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. ---
**Author:** ![plragde](https://avatars.discourse-cdn.com/v4/letter/p/ac8455/32.png) [@plragde](https://racket.discourse.group/u/plragde)\ **Post date:** [December 3, 2021, 9:25pm UTC](https://racket.discourse.group/t/new-chapter-in-logic-and-computation-intertwined/338/5 "2021-12-03T21:25:45Z")
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](https://cs.uwaterloo.ca/~plragde/flaneries/FIMS/index.html) ---
**Author:** ![countvajhula](https://yyz2.discourse-cdn.com/free1/user_avatar/racket.discourse.group/countvajhula/32/65_2.png) [@countvajhula](https://racket.discourse.group/u/countvajhula)\ **Post date:** [December 3, 2021, 9:54pm UTC](https://racket.discourse.group/t/new-chapter-in-logic-and-computation-intertwined/338/6 "2021-12-03T21:54:33Z")
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](https://dl.acm.org/doi/abs/10.1145/2975980.2975981)