Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Stefan Monnier <monnier@iro.umontreal.ca>
Newsgroups: comp.arch
Subject: Re: Computer architects leaving Intel...
Date: Mon, 09 Sep 2024 15:55:32 -0400
Organization: A noiseless patient Spider
Lines: 18
Message-ID: <jwvwmjkmwss.fsf-monnier+comp.arch@gnu.org>
References: <2024Aug30.161204@mips.complang.tuwien.ac.at>
	<memo.20240830164247.19028y@jgd.cix.co.uk>
	<vasruo$id3b$1@dont-email.me>
	<jwv7cbxq2xb.fsf-monnier+comp.arch@gnu.org>
	<vav7dd$11ep6$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain
Injection-Date: Mon, 09 Sep 2024 21:55:46 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="838e8b1b23b20f4114a05b2e131ca424";
	logging-data="2667997"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1/U7gNfeKn+qPpGD2YiqlO6Pqlsc7ti9Bk="
User-Agent: Gnus/5.13 (Gnus v5.13)
Cancel-Lock: sha1:7bzzG03GuSNzHEcih+f+G1wdyxc=
	sha1:LjFxevVmOxq6kTRWI2XHx8TNG3k=
Bytes: 1945

>> 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