> 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 :)
> 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.
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.
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 :)