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.

Cars are similar to planes in that they're very complex electric/mechanical machines. They have lots of code where if it is done poorly (Toyota spaghetti code acceleration nightmare) people could be seriously injured or even die. Tesla isn't the only car company, but has a pretty strong fan base. The poster is just generalizing the OP to car software. Seems relevant to me.

If all you think about is Tesla, every comment thread is a relevant place to post.