Interestingly, the last slide mentions: ``` Today: we are able to certify realistic bytecode compilers and abstract machines. Tomorrow: certification of optim

Interestingly, the last slide mentions: ``` Today: we are able to certify realistic bytecode compilers and abstract machines. Tomorrow: certification of optimizing native-code compilers? ``` Xavier Leroy actually got the ACM Software System Award in 2021 for CompCert, an optimizing native-code compiler! It's first version seems to have been released in 2005, just 3 years after this presentation was written. Though CompCert is a C compiler, which isn't really a functional language. - https://en.wikipedia.org/wiki/ACM_Software_System_Award https://en.wikipedia.org/wiki/ACM_Software_System_Award - https://en.wikipedia.org/wiki/CompCert https://en.wikipedia.org/wiki/CompCert