Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.c > #400176 > unrolled thread

Re: Constants and undefined behavior

Back to article view | Back to comp.lang.c

This discussion starts older than the indexed window; earlier articles aren't shown. The article labeled Started by below is the oldest one visible, not the original post.

Contents

  Re: Constants and undefined behavior Tim Rentsch <tr.17687@z991.linuxsc.com> - 2026-06-21 15:26 -0700
    Re: Constants and undefined behavior antispam@fricas.org (Waldek Hebisch) - 2026-06-22 03:40 +0000
      Re: Constants and undefined behavior Tim Rentsch <tr.17687@z991.linuxsc.com> - 2026-08-15 07:50 -0700

#400176 — Re: Constants and undefined behavior

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?

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

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

[toc] | [next] | [standalone]

#400181

Tim Rentsch <tr.17687@z991.linuxsc.com> 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.

-- 
                              Waldek Hebisch

[toc] | [prev] | [next] | [standalone]

#401210

antispam@fricas.org (Waldek Hebisch) writes:

> Tim Rentsch <tr.17687@z991.linuxsc.com> 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.

[toc] | [prev] | [standalone]

Back to top | Article view | comp.lang.c

csiph-web