Not usually in the habit of giving much thought to Tesla, but suggesting that a proven correct C compiler created by a company that builds transportation devic

Not usually in the habit of giving much thought to Tesla, but suggesting that a proven correct C compiler created by a company that builds transportation devices that contain lots of computers might be interesting for another company that builds transportation devices that use lots of computers seems to me to be perfectly sensible. Especially since that other company has a bit of a reputation for writing shoddy software. In fact, the more I think about the more relevant this comment becomes. Building computerized transportation devices is hard and apparently one of the things you need to do it well is a proven correct C compiler. A far cry from the type of software development most people do, which involves slapping together some stuff we found on the internet and writing some glue code around it.