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
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!