<p><span class="h-card" translate="no"><a href="https://functional.cafe/@racketlang" class="u-url mention">@<span>racketlang</span></a></span> Thanks for the boost! I apologize that the last chapter is still incomplete. Racketeers may also be interested in the complete LACI (Logic and Computation Intertwined), which prepares one for Agda or Coq by constructing a small proof assistant (Proust) in Racket.</p><p><a href="https://cs.uwaterloo.ca/~plragde/flaneries/LACI/" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">cs.uwaterloo.ca/~plragde/flane</span><span class="invisible">ries/LACI/</span></a></p>