[globuous]

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/CompCert

[hayley-patton]

CakeML is a formally verified implementation of a subset of Standard ML which generates native code. Not sure about what it optimises though.