Highlight of #POPL yesterday: seeing some excellent discussions of Coq for verifying programming languages! https://popl20.sigplan.org/details/PLMW-POPL-2020/3/Theorem-provers-are-a-P-L-researcher-s-best-friend I came away with a much clearer sense of *how* you'd verify an optimising compiler.