[Cryptech Tech] The compcert compiler

[Rob Austein]

On Wed, 23 Jan 2019 14:16:22 -0500, Joachim Strömbergson wrote:
> 
> This appeared on HN yesterday. A formally verified compiler. It can
> generate code for ARM. Something we could use perhaps?
> 
> http://compcert.inria.fr/

I would not object if someone were to contribute code showing how to
use that compiler as an alternative to gcc, but it's not free software
(download page says "no commercial use"), so switching to it entirely
seems problematic.

Unclear how close it is to being a drop-in replacement for
gcc. Command line syntax as shown in the manual is very gcc-like, but
stm32 builds use enough fiddly gcc options that there are likely to be
divergences, the questions would be how serious and how hard to fix.