[millstone]

That's a great point. Often you need to run your system in simulation via a model. Generating the code directly from the model is one way to prove that your system matches the simulation.

Of course the modeling tools speak mostly C. This illustrates how C's weaknesses are mitigated in practice, and how much work prospective C-replacements must do to be competitive.

[kbenson]

> This illustrates how C's weaknesses are mitigated in practice

Except there's likely a false sense of security in how well those mitigations work. Part of the problem with C is that later optimizations by the compiler can yield insecure code at a later date because of undefined behavior and compiler optimization techniques that take advantage of it. In other words, if your generated code takes advantage of any undefined behavior, there's no guarantee that the same code compiler on the same compiler with the same flags but with a different/newer version of that compiler will yield bug free code in both cases.

Can those models produce C code with absolutely no undefined behavior? Maybe? When's the last time someone did a close look at exactly what they were generating? Did they make sure to look again when the underlying architecture changed (even from one version of ARM to another...)?

See the somewhat recent Cap'N'Proto remote vuln[1] submission for a modern case of this, and a good discussion of the problem in detail.

1: https://news.ycombinator.com/item?id=14163111

[hsjoberg]

Yeah testing needs to be done with compiled code on target card otherwise you can't be sure it works. Usually compiling code is super strict no further optimization then the standard can be used etc. Only specific cards and compilers are "trusted" to use.

[hsjoberg]

Yes and the code/models go through extensive testing. Everyone in the industry knows that a callback because of faulty software will cost an insane amount of money. This is changing a bit since more and more work is going towards over-the-air update.