Sujet : Re: Computer architects leaving Intel...
De : monnier (at) *nospam* iro.umontreal.ca (Stefan Monnier)
Groupes : comp.archDate : 09. Sep 2024, 20:55:32
Autres entêtes
Organisation : A noiseless patient Spider
Message-ID : <jwvwmjkmwss.fsf-monnier+comp.arch@gnu.org>
References : 1 2 3 4 5
User-Agent : Gnus/5.13 (Gnus v5.13)
So it's all up to the programmer, who often doesn't know either.
Other than using CompCert, I don't know of any reliable way for
a programmer to make sure his C code does not suffer from UB.
There is no full-proof or complete method for C. There are other language
for which formal methods can come closer to proving the correctness of the
code, but for most practical cases this is infeasible.
I'm not talking about proving that your code is correct. I'm talking
about making sure that your code can do only those things that you
wrote, as opposed to the situation with UB which includes all behaviors
including those not written in your code.
Any strongly typed language (Javascript, Python, Java, Haskell, ...)
gives you such a guarantee with absolutely no effort required on the
part of the programmer.
Stefan