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
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:
2
2
13
Nice, code looks really clean!
1
2
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!