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. _______________________________________________ Tech mailing list Tech@cryptech.is https://lists.cryptech.is/listinfo/tech
