Path: ...!weretis.net!feeder9.news.weretis.net!news.quux.org!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: Richard Heathfield <rjh@cpax.org.uk>
Newsgroups: comp.theory
Subject: =?UTF-8?Q?Re=3A_Flibble=E2=80=99s_Leap=3A_Why_Behavioral_Divergence?=
 =?UTF-8?Q?_Implies_a_Type_Distinction_in_the_Halting_Problem?=
Date: Mon, 12 May 2025 05:12:13 +0100
Organization: Fix this later
Lines: 100
Message-ID: <vvrsev$tfq2$1@dont-email.me>
References: <vv1UP.77894$JJT6.54808@fx16.ams4> <vvqd4u$g8a1$1@dont-email.me>
 <7N2UP.527443$wBt6.464256@fx15.ams4> <vvqfgq$gmmk$1@dont-email.me>
 <os3UP.670056$BFJ.223954@fx13.ams4> <vvqgpt$gmmk$4@dont-email.me>
 <aG3UP.366972$wBVe.321504@fx06.ams4>
 <39947848bf73be52ee6fbbeb6d0d929009dfec8e@i2pn2.org>
 <fR8UP.92502$o31.50010@fx04.ams4>
 <fb3915123ad5c4703b92df902c37267fce2c4812@i2pn2.org>
 <vvrhk6$nejb$2@dont-email.me> <vvrhtj$nnmf$1@dont-email.me>
 <43f0f4158610d859516ba3e0115a8a2b8bd7630b@i2pn2.org>
 <vvrl9h$o2ab$6@dont-email.me> <vvrmso$nt1l$2@dont-email.me>
 <87frha4j5w.fsf@nosuchdomain.example.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Mon, 12 May 2025 06:12:16 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="c9b9500fbbca16233fc3a49bed1da056";
	logging-data="966466"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+lQYgBGF8O2nCaPn9E3yuPr8SeTL4QcpaDbxRBl+DHcQ=="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:ArD8jAmtMnioVUNrBwVw0lIYphs=
In-Reply-To: <87frha4j5w.fsf@nosuchdomain.example.com>
Content-Language: en-GB
Bytes: 5884

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