Path: csiph.com!eternal-september.org!feeder.eternal-september.org!nntp.eternal-september.org!.POSTED!not-for-mail From: Tim Rentsch Newsgroups: comp.lang.c Subject: Re: Constants and undefined behavior Date: Sat, 15 Aug 2026 07:50:28 -0700 Organization: A noiseless patient Spider Lines: 96 Message-ID: <867blr5tfv.fsf@linuxsc.com> References: <10v7b32$2u85v$1@dont-email.me> <10vt7b9$pi3s$1@kst.eternal-september.org> <110032s$clq$1@reader1.panix.com> <1100g0e$1lt8i$1@kst.eternal-september.org> <11058u3$mv5$1@reader1.panix.com> <1107q1e$ccfa$1@paganini.bofh.team> <110eht5$1naub$5@dont-email.me> <110enrj$15fs1$1@paganini.bofh.team> <110f05e$1nauc$8@dont-email.me> <110fqco$1ck3s$3@paganini.bofh.team> <868q878r8k.fsf@linuxsc.com> <111aas6$vtir$1@paganini.bofh.team> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Injection-Date: Sat, 15 Aug 2026 14:50:31 +0000 (UTC) Injection-Info: dont-email.me; logging-data="3635087"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/5X5tPPjgeD1sb8dzLo2y+dFwvQ/MhSU0="; posting-host="f88cfb7384c39afe54609bf3101f3803" User-Agent: Gnus/5.11 (Gnus v5.11) Emacs/22.4 (gnu/linux) Cancel-Lock: sha1:exQG8M11ybZWiFMwZew+/Hvz824= sha1:B1ar5pO5+IiFmK7kEWedECqQ9Zc= sha256:mQQJTVVBWiHe2E//Ab9s2i9PoWeNYggj6BF510YobAU= sha1:bAkqJZ4jg8kLIoq6Zxq885/iCPg= sha256:Az1dHFUlSjX6NCDJS24FTWZbqhN2tPvYfe4nx65k4g4= Xref: csiph.com comp.lang.c:401210 antispam@fricas.org (Waldek Hebisch) writes: > Tim Rentsch wrote: > >> antispam@fricas.org (Waldek Hebisch) writes: >> >> [...] >> >>> I think that lawyerish style of current C standard is mostly >>> inertia, >> >> I wouldn't use a term like lawyerish to describe the text in the >> ISO C standard. Can you explain what quality you mean to ascribe >> to "lawyerish" writing in the C standard without using any term >> related to lawyering or legal documents? > > Sorry no, I can not. My point is that you need to treat > C standard almost like legal document and I can not explain > this without using proper terminology. > >>> and making standard more mathematical would improve it. >> >> Could you elaborate on that statement? In what ways would giving >> a more mathematical treatment of C semantics improve the quality >> of the ISO C document? How would doing that advance the stated >> purposes or goals of the C standard? > > There are many aspect of mathematical treatment. One is care > about terminology, namely that terms are either reasonably > clearly marked as "primitve" (and assumed to be understood > by readers) or are precisely defined. Related is that > words can be taken as written, without needing to look at > intent or similar legal style arguments. You may think that > C standard already posseses such properties, but recent > example, that is definition of expression nicely illustrates > current problems. With mathematical treatment expression > would be part of C program derived from corresponding > grammar rule and that would resolve the problem. In the > past in this group there were several discussions about > various parts of C standard, and there were cases were > standard wording looked genuinly confusing. I am not > prepared to dig into those discussions, but my impression > was that in some cases mathematical treatment would make > things clearer. > >>> But giving formal semantic in the standard would mean >>> significantly bigger change. >> >> Due to the nature of C, I believe it is effectively impossible to >> give a formal mathematical definition of the semantics of C. Do >> you think such a thing is feasible or practicable? If so can you >> explain the reasoning behind your thinking? > > I think that this is possible given dedicated team of qualified > people doing the work. I do not know if it is practically > possible to assemble needed team. I already mentioned axiomatic > semantics. There is C grammar and we need to assign semantics > to various production rules. We do this assigning precondtions > and postcondtions to the rules. In much simpler cases this > was done. C is bigger language and rules are more complicated, > but that for me looks like quantitive problem, that is there is > more work and result will be bigger. Clearly, this would > require buy-in from the standard body. Namely, formalization > is likely to uncover many unclear places in C standard and > ensuring that formalization matches the standard would require > resolution by the standard body. It is quite possible that > standard body would refuse to cooperate. To explain this more, > let me mention past discussion about Extended Pascal in a > different forum. I was looking at types of constants, but in > specific case rules looked contradictory, so I asked a > question. One response was from former commitee member (this > was several years after Pascal standard was ratified), he > basicaly said that type of constants does not matter. Which > was mostly true, but my reason for asking the question was > that validity of programs depended on types of constants. > Something similar may happen during formalization: > formalization may discover unclear places in C standard > which C commitee considers irrelevant in practice and > refuses to clarify. > > BTW: Authors of some tools already need and have formal > semantics for language rather close to C. Namely, > Comp-Cert compiler is matching conditions in source > code with machine code and for that it needs reasonably > good aproximation to formal semantics of language implemented > by C compiler (more precisely gcc). Microsoft developed > formal checking tools and that too needs formal semantics. > But since goals are different neither give semantics of > standard C. A disappointing response. You can't explain what you mean. The properties ascribed to a mathematical writing might just as well be met by more clearly written English. About defining a formal semantics, all you really say is you think it is possible, under some not very well defined conditions. All in all not too compelling.