4 ms·

One issue with this is that the text of the C standard isn't actually enough to unambiguously determine what the committee (and compiler vendors) intend for the

One issue with this is that the text of the C standard isn't actually enough to unambiguously determine what the committee (and compiler vendors) intend for the language to mean in practice. The official standards mailing lists for C and C++ are constantly filled with issues regarding inconsistencies in the ISO standards, and for C++ at least people often resort to trying a code sample in multiple major compilers to decide what it's "supposed to do" when the standard is unclear. It might be a bit better with C, but I once tried to start implementing a toy C++ compiler by following the text of the standard literally and it became impossible pretty quickly. There are so many pieces where you are just expected to know what they intend and what inconsistencies can be ignored because you're already familiar with the language that it would be difficult to call any one person's interpretation a formalization of the standard itself.

thinkpad20 11y ago
> the text of the C standard isn't actually enough to unambiguously determine what the committee (and compiler vendors) intend for the language to mean in practice. Interesting! If the standard is under-specified, then presumably this student must have had to fill in some of the holes themselves, or found a way to represent multiple interpretations simultaneously. > issues regarding inconsistencies in the ISO standards If the standards are inconsistent (in a logical sense), and this formalization is sufficiently complete, it should uncover those inconsistencies since they would amount to type errors in Coq. I wonder if the author had any of those difficulties. > trying a code sample in multiple major compilers to decide what it's "supposed to do" when the standard is unclear One of the effects a project like this could have is to make this (at least theoretically) unnecessary to do. > implementing a toy C++ compiler by following the text of the standard literally and it became impossible pretty quickly Fortunately C is a much smaller and simpler language than C++. Isn't the C++ standard almost 1000 pages? I'm not sure what the C standard is but it must be quite a bit smaller. Regardless, it's a PhD thesis so the difficulty of the task isn't a reason not to attempt it :)
- nly 11y ago
  > Fortunately C is a much smaller and simpler language than C++. Isn't the C++ standard almost 1000 pages? The language specification itself is only about ~450 pages, the rest is library. It of course inherits all of the insanity of C on top of that (~170 pages of C language spec), which I'd argue brings a disproportionately large share of the pain. Alex's point is that the standard doesn't really begin to give you an idea how hard it is to write an implementation, or make decisions about everything that's unspecified or ambiguous.
  - _kst_ 11y ago
    The C standard doesn't exactly "inherit" the 170 pages of the C language spec. As far as I know, the core C++ language (excluding the library) is defined entirely by the C++ standard, without reference to the C standard. It was certainly based on C, but the description doesn't depend on it. The C standard library is incorporated by reference (with a few tweaks) into the C++ standard. Of course the C++ standard library also includes a lot of material that isn't in the C standard library.
nly 11y ago
This isn't unusual in software. There are still ambiguities around edge-cases in surprisingly important specifications. For instance, apparently, even after 20 years of HTTP we still can't be sure we've nailed down a correct grammar[0]. I'm also in possession of a DNS zone file (a format that was very loosely specified going on 30 years ago) that is parsed 3 different ways by 3 different vendors. [0] https://www.rfc-editor.org/errata_search.php?rfc=7230&eid=4189 https://www.rfc-editor.org/errata_search.php?rfc=7230&eid=41...

thinkpad20 11y ago

> the text of the C standard isn't actually enough to unambiguously determine what the committee (and compiler vendors) intend for the language to mean in practice. Interesting! If the standard is under-specified, then presumably this student must have had to fill in some of the holes themselves, or found a way to represent multiple interpretations simultaneously. > issues regarding inconsistencies in the ISO standards If the standards are inconsistent (in a logical sense), and this formalization is sufficiently complete, it should uncover those inconsistencies since they would amount to type errors in Coq. I wonder if the author had any of those difficulties. > trying a code sample in multiple major compilers to decide what it's "supposed to do" when the standard is unclear One of the effects a project like this could have is to make this (at least theoretically) unnecessary to do. > implementing a toy C++ compiler by following the text of the standard literally and it became impossible pretty quickly Fortunately C is a much smaller and simpler language than C++. Isn't the C++ standard almost 1000 pages? I'm not sure what the C standard is but it must be quite a bit smaller. Regardless, it's a PhD thesis so the difficulty of the task isn't a reason not to attempt it :)

nly 11y ago
> Fortunately C is a much smaller and simpler language than C++. Isn't the C++ standard almost 1000 pages? The language specification itself is only about ~450 pages, the rest is library. It of course inherits all of the insanity of C on top of that (~170 pages of C language spec), which I'd argue brings a disproportionately large share of the pain. Alex's point is that the standard doesn't really begin to give you an idea how hard it is to write an implementation, or make decisions about everything that's unspecified or ambiguous.
- _kst_ 11y ago
  The C standard doesn't exactly "inherit" the 170 pages of the C language spec. As far as I know, the core C++ language (excluding the library) is defined entirely by the C++ standard, without reference to the C standard. It was certainly based on C, but the description doesn't depend on it. The C standard library is incorporated by reference (with a few tweaks) into the C++ standard. Of course the C++ standard library also includes a lot of material that isn't in the C standard library.

nly 11y ago

This isn't unusual in software. There are still ambiguities around edge-cases in surprisingly important specifications. For instance, apparently, even after 20 years of HTTP we still can't be sure we've nailed down a correct grammar[0]. I'm also in possession of a DNS zone file (a format that was very loosely specified going on 30 years ago) that is parsed 3 different ways by 3 different vendors. [0] https://www.rfc-editor.org/errata_search.php?rfc=7230&eid=4189 https://www.rfc-editor.org/errata_search.php?rfc=7230&eid=41...