Do any of you have a favorite homework exercise for a formal proof of compiler correctness in Coq? Searching for one publicly available to send to students to onboard for a research project, and possibly play with and change in interesting ways
Conversation
Replying to
I enjoyed doing the arithmetic expression compiler exercise here: courses.ps.uni-saarland.de/sem_ws1718/3/R - took me a long time and had to ask for a lot of help on the /r/PL discord, but it was fun! I did it in Lean 4:
I need to get around to learning how to do more complicated stuff! I'd like to eventually play around with typed assembly language for example. But yeah I always make life hard for myself by trying to both learn theorem proving *and* port Coq to Lean at the same time!
Thanks! Yeah that's one thing I like about Lean. The approach to namespacing and the more consistent code style (while still evolving), make it much easier to keep things clean and readable. I wish some things were different, but I still think there's a lot to love!
1