halt (p, i)
{ if ( program p halts on input i )
return true ; // p halts
else
return false ; // p doesn’t halt
} Fig. 1. Pseudocode of the Halting Function

Strachey’s Impossible Program Strachey proposed a program
based on the result of an assumed halting function [2].
The way Strachey’s construction and other similar constructions
are used to show the impossibility of a decideable halting
function is quite similar to Turing’s original disproof.
But the relevant difference we want to emphasize is that
they do not explicitly assume an infinite number of possible
machines (programs) or input data, because they directly use
reductio ad absurdum to prove that both, Strachey’s construction
and the universal halting function cannot exist.

strachey ( p )
{ if ( halt (p, p) == true )
L1 : goto L1 ; // loop forever
else
return;
}

Fig. 2. Strachey’s Impossible Program

The impossibility of Strachey’s construction given in Figure 2 becomes
obvious if one tries to apply the halting function as follows:

halt(strachey, strachey)

Since in this case strachey() itself calls halt(strachey, strachey),
it is required that the direct call of halt() and the nested call
provide the same result. However, this leads to a contradiction,
whatever result halt() returns. Within this disproof there seems
to be no indication why not it could be even applied to finite-state
systems having a concrete upper bound of state space.

https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.206.1468&rep=rep1&type=pdf

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

On 7/8/2021 3:27 PM, olcott wrote:
>
> halt (p, i)
> {
>   if ( program p halts on input i )
>     return true ; // p halts
>   else
>     return false ; // p doesn’t halt
> }
> Fig. 1. Pseudocode of the Halting Function
>
> Strachey’s Impossible Program Strachey proposed a program
> based on the result of an assumed halting function [2].
> The way Strachey’s construction and other similar constructions
> are used to show the impossibility of a decideable halting
> function is quite similar to Turing’s original disproof.
> But the relevant difference we want to emphasize is that
> they do not explicitly assume an infinite number of possible
> machines (programs) or input data, because they directly use
> reductio ad absurdum to prove that both, Strachey’s construction
> and the universal halting function cannot exist.
>
> strachey ( p )
> {
>   if ( halt (p, p) == true )
>     L1 : goto L1 ; // loop forever
>   else
>     return;
> }
>
> Fig. 2. Strachey’s Impossible Program
>
> The impossibility of Strachey’s construction given in Figure 2 becomes
> obvious if one tries to apply the halting function as follows:
>
> halt(strachey, strachey)
>
> Since in this case strachey() itself calls halt(strachey, strachey),
> it is required that the direct call of halt() and the nested call
> provide the same result. However, this leads to a contradiction,
> whatever result halt() returns. Within this disproof there seems
> to be no indication why not it could be even applied to finite-state
> systems having a concrete upper bound of state space.
>
> https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.206.1468&rep=rep1&type=pdf
>
>

The link is too long so I posted the whole letter:

Strachey, C.: An impossible program.
Computer Journal 7(4), 313 (1965)

To the Editor,
The Computer Journal.

An impossible program

Sir,
A well-known piece of folk-lore among programmers
holds that it is impossible to write a program which can
examine any other program and tell, in every case, if it
will terminate or get into a closed loop when it is run.
I have never actually seen a proof of this in print, and
though Alan Turing once gave me a verbal proof (in a
railway carriage on the way to a Conference at the
NPL in 1953), I unfortunately and promptly forgot the
details. This left me with an uneasy feeling that the
proof must be long or complicated, but in fact it is so
short and simple that it may be of interest to casual
readers. The version below uses CPL, but not in any
essential way.

Suppose T[R] is a Boolean function taking a routine
(or program) R with no formal or free variables as its
argument and that for all R, T[R] — True if R terminates
if run and that T[R] = False if R does not terminate.
Consider the routine P defined as follows

rec routine P
§L:if T[P] go to L
Return §

If T[P] = True the routine P will loop, and it will
only terminate if T[P] = False. In each case T[P] has
exactly the wrong value, and this contradiction shows
that the function T cannot exist.

Yours faithfully,
C. STRACHEY
Churchill College,
Cambridge.

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

This is the official link to the original letter:
https://academic.oup.com/comjnl/article/7/4/313/354243

Strachey is responsible for the enormous simplification of the halting
problem proof that is widely distributed as pseudo code.

His version was written in the language that he created CPL.
This language was later transformed into BCPL, then B then C.

CPL (Combined Programming Language) is a multi-paradigm programming
language, that was developed in the early 1960s. It is an early ancestor
of the C language via the BCPL and B languages.
https://en.wikipedia.org/wiki/CPL_(programming_language)

Strachey, C.: An impossible program.
Computer Journal 7(4), 313 (1965)

To the Editor,
The Computer Journal.

An impossible program

Sir,
A well-known piece of folk-lore among programmers
holds that it is impossible to write a program which can
examine any other program and tell, in every case, if it
will terminate or get into a closed loop when it is run.
I have never actually seen a proof of this in print, and
though Alan Turing once gave me a verbal proof (in a
railway carriage on the way to a Conference at the
NPL in 1953), I unfortunately and promptly forgot the
details. This left me with an uneasy feeling that the
proof must be long or complicated, but in fact it is so
short and simple that it may be of interest to casual
readers. The version below uses CPL, but not in any
essential way.

Suppose T[R] is a Boolean function taking a routine
(or program) R with no formal or free variables as its
argument and that for all R, T[R] — True if R terminates
if run and that T[R] = False if R does not terminate.
Consider the routine P defined as follows

rec routine P
§L:if T[P] go to L
Return §

If T[P] = True the routine P will loop, and it will
only terminate if T[P] = False. In each case T[P] has
exactly the wrong value, and this contradiction shows
that the function T cannot exist.

Yours faithfully,
C. STRACHEY
Churchill College,
Cambridge.

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein