Rooster and its place in computing
Coq, proof assistant

In 2013, Coq received two awards from the Association for Computing Machinery (ACM), the SIGPLAN "Programming Languages Software Award" and the prestigious "Software System Award". The text accompanying this second award places Coq in the context of correct software production. The full text can be found on the ACM website :

"Coq, used for both mathematical theorems and software specifications, is a key technology for the production of certified software.

Significant results achieved with Coq include the proof of the Four Color Theorem, the development of CompCert (a fully verified compiler for C), the development at Harvard...