```
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.
``` 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