Re: Flibble’s Leap: Why Behavioral Divergence Implies a Type Distinction in the Halting Problem

On 12/05/2025 04:11, Keith Thompson wrote:

Richard Heathfield <rjh@cpax.org.uk> writes:
[...]

ALL C compilers are required to diagnose ALL syntax errors and ALL
constraint violations.

 Yes, all conforming C compilers are required to do that.  (Well,
strictly speaking they're only required to issue at least one diagnostic
for any translation unit that violates a syntax rule or constraint.)

I was unintentionally ambiguous, for which I apologise.
The point I sought to make is that there is no syntax error (or constraint violation) so trivial that a compiler is given licence not to issue a diagnostic it if it has no other reason so to do.
That is, they are all capable of ticking the box that says 'must issue at least one diagnostic'.

 [...]
 

In my experience, Microsoft's C compiler - although not perfect - is
pretty good at following conformance rules. I'd be surprised to learn
from a competent source that it misses a syntax error.

 I wouldn't, since few if any C compilers are conforming by default.

I was talking about conforming mode, which IIRC (it's been a while) is invoked by -W4 (a warning level that I habitually used in the days when I still used Microsoft software).

I've just tried 4 different C compilers (gcc, clang, and tcc
on Ubuntu, MS Visual Studio 2022 on Windows), and none of them
diagnosed a stray semicolon at file scope *by default*.  gcc and
clang can be persuaded to diagnose it.  tcc, as far as I can tell,
cannot; I don't believe it claims to be fully conforming in any mode.
I wasn't able to get MSVS to diagnose it, but there could easily
be an option that I'm missing.

Could you crank MSVS up to -W4 (or whatever the max is these days) and try again? I hate to impose, but of course it's your own fault for qualifying as a competent source. ;-)
If it doesn't diagnose at its maximum warning level, then okay, ~I lose the syntax battle.

If I wanted to prove something in mathematical logic using C code as
a vehicle, I personally would try to use fully standard-conforming C.

So would I, if only to fend off pedantic fuss-pots such as... well, me, I suppose...
[Aside: I just checked what I laughingly call my archives to verify this, and I found an old (and I do mean ancient) Monty Hall simulation - 100 lines of C that gcc wasn't too pleased with when I turned on nanny mode, but which I'd be perfectly happy to defend before the X3J11 committee.
100 lines isn't much, of course, but it was throwaway code, so I had less motivation than usual to follow the rules, but follow them I still did.]
...and also to eliminate a potential source of error. Why tempt fate?

I *might* consider using a more lax C-like language, such as the
language accepted by some C compiler in its default mode -- but I'd
need a good reason to do that, and I'd want a rigorous definition
of anything I use that differs from standard C.

Likewise.
I'd also steer clear of basing a mathematical proof on a program that is sensitive to the file formats of a particular platform. I'd need an *astoundingly* good reason to do that.

 It's possible that olcott's C-like code has well defined behavior
in the implementation he's using.  If so, I'm not sure there's any
fundamental reason to use something close to C rather than using C
itself in an attempted refutation of some well known mathematical
proof.  (I wouldn't expect either C or something C-like to be a
good vehicle for such a proof.  I don't think C is defined rigorously
enough to be useful for such a task, and any C-like language is even
less so.)

FYI Agda, Lean, and Rocq all offer proof vehicles, and all three are likely to be better suited to the task than is C.

olcott will likely use this to claim that I support his views.
He will be wrong.

It hardly matters. A crank is a crank is a crank.
--
Richard Heathfield
Email: rjh at cpax dot org dot uk
"Usenet is a strange place" - dmr 29 July 1999
Sig line 4 vacant - apply within