On 30/01/2023 10:00, John Levine wrote:
> [Remember that while the halting problem is insoluble in general, it's
> often soluble in specific cases, e.g. "halt" or "foo: goto foo".

More usefully, there are methods for transforming a formal
specification into an executable implementation which
preserve semantic equivalence, and therefore are guaranteed
to produce a terminating program (for input states for which
the specification is defined). For example:

"Provably Correct Derivation of Algorithms Using FermaT"
Martin Ward and Hussein Zedan
Formal Aspects of Computing, September 2014.
Volume 26, Issue 5, Pages 993--1031, 2014-09-01, ISSN: 0934-5043
doi:dx.doi.org/10.1007/s00165-013-0287-2
http://www.gkc.org.uk/martin/papers/trans-prog-t.pdf

> Nevertheless, I would be quite surprised if anyone could prove a
> non-toy translator correct. -John]
According to this paper: "The state of the art [as of 2014] is
the CompCert compiler, which compiles almost all of the C language
to PowerPC, ARM and x86 assembly and has been mechanically verified
using the Coq proof assistant."

Xavier Leroy. "Formally verifying a compiler: Why? How? How far?".
CGO 2011 - 9th Annual IEEE/ACM International Symposium on Code
Generation and Optimization, Apr 2011, Chamonix, France.
⟨10.1109/CGO.2011.5764668⟩. ⟨hal-01091800⟩

https://hal.inria.fr/hal-01091800

--
Martin

Dr Martin Ward | Email: martin@gkc.org.uk | http://www.gkc.org.uk
G.K.Chesterton site: http://www.gkc.org.uk/gkc | Erdos number: 4

I've never understood this. Isn't there a chicken and egg problem?
How do we know that the theorem prover is correct and bug free?

I ask in all seriousness.

Thanks,

Arnold

In article <23-01-092@comp.compilers>, Martin Ward <martin@gkc.org.uk> wrote:
>On 30/01/2023 10:00, John Levine wrote:
>> [Remember that while the halting problem is insoluble in general, it's
>> often soluble in specific cases, e.g. "halt" or "foo: goto foo".
>
>More usefully, there are methods for transforming a formal
>specification into an executable implementation which
>preserve semantic equivalence, and therefore are guaranteed
>to produce a terminating program (for input states for which
>the specification is defined). ...
[It's a perfectly reasonable question. Alan Perlis, who was my thesis
advisor, never saw any reason to believe that a thousand line proof
was any more likely to be bug-free than a thousand line program.
-John]

On 01 Feb 2023 08:07:24 GMT
arnold@freefriends.org (Aharon Robbins) wrote:
> I've never understood this. Isn't there a chicken and egg problem?
> How do we know that the theorem prover is correct and bug free?

We prove it by hand ? I don't know if anyone has done this for the
provers mentioned but it feels like a feasible task and when it's done ,
it's done i.e. a theorem prover is not the kind of software which
continually gets updated.

> [It's a perfectly reasonable question. Alan Perlis, who was my thesis
> advisor, never saw any reason to believe that a thousand line proof
> was any more likely to be bug-free than a thousand line program.
> -John]

It depends on what we mean by "bug" , in mathematics we wouldn't say "bug"
but "error".

First you have *typos* which is situations where one was meaning to , for
example , write i and they wrote j instead. It may be that mathematics
proofs have more of those than computer programmes because in computer
programmes some will be caught by the compiler like for example if j has
not been declared. But the essential difference is that a typo is harmless in
mathematics , the reader of the proof will either notice and understand what
was intended or even unconsciously replace what is written with what was
intended. But in computer programmes this kind of typo bug can be
catastrophic. Hence in mathematics we wouldn't say that a proof has errors
just because it has a typo , we would say it has a typo.

For other errors , logic errors , I would guess that computer programmes will
have more errors/bugs than mathematical proofs. This assertion is based on
personal experience and instinct to some extent , having written both many
programmes and many proofs. But I will attempt to give some of what I think
are reasons :

1:
In mathematics you work with a formalism right from the start but in computer
programmes often one has an intuitive understanding of what the program is
meant to achieve and a working programme may be considered to have a bug when
its behaviour turns out not to match closely enough that intuitive
understanding. The difference in the level of formalism is not just about
the programmes but about the programming languages too. In standards of
programming languages I've read , the language is not described in precise
mathematical detail. The grammar usually is but not other parts of the language.

For example , from the C standard :
The result of the binary + operator is the sum of the operands.

Even just for integer arguments , this is nowhere a complete definition but
to piece together a complete definition one must combine information
scattered in faraway parts of the standard. This would never occur in a
mathematics books or paper , the complete definition of a function or
operator or whatever (including the precise set for which it is defined)
would appear in one place. This sort of thing where one has to piece
together information from many parts of the document to arrive at a complete
definition , seems to be common in computer language standards and I have
no idea why it happens , I don't think anything about specifying a programming
language forces things to be done like this. But the result is that programmers
will often work with a mix of precise specification and intuitive understanding
of the language they're using.

2:
In mathematics a correct proof *is* the goal but in computer programming some
set of behaviours is the goal and the set of behaviours may not even be the
ultimate goal but the desire to make a profit is. For example

en.wikipedia.org/wiki/Pac-Man :
Due to an integer overflow, the 256th level loads improperly, rendering
it impossible to complete.

But this didn't prevent the game from being highly successful. "Donkey Kong"
also had a bug which prevented progress from some point onwards.

What is the goal also influences the kind of people who specialise in computer
programming vs those who write mathematical proofs. My impression is that there
exist computer programmers who are of the "trial and error" type who write some
code which seems to approximate what they have in mind , test it , write some
more code and so forth. Eventually they arrive at something which seems to
match their mental model and they consider themselves done. They wouldn't have
any interest and possibly ability to write a proof of correctness. As a practical
matter , they may be perfectly productive and write code which works for the
desired cases.

3:
There is a kind of bug/error for which there's no mathematical analogue :

From "Expert C Programming" by Peter van der Linden :

One release of an ANSI C compiler had an interesting bug. The symbol
table was accessed by a hash function that computed a likely place from
which to start a serial search. The computation was copiously commented,
even describing the book the algorithm came from. Unfortunately, the
programmer omitted to close the comment! The entire hash initial value
calculation thus fell inside the continuing comment,

[...]

The entire calculation of the initial hash value was omitted, so the
table was always searched serially from the zeroth element! As a result,
symbol table lookup (a very frequent operation in a compiler) was much
slower than it should have been. This was never found during testing
because it only affected the speed of a lookup, not the result. This is
why some compilers complain if they notice an opening comment in a
comment string. The error was eventually found in the course of looking
for a different bug. Inserting the closing comment resulted in an
immediate compilation speedup of 15%!

[The history of formal description of programming languages is not
encouraging. Back in the 1970s the ANSI PL/I standard was defined in
terms of formal operations on trees, but even so it had bugs/errors.
Also, per your comment on addition, in a lot of cases the practical
definition turns into whatever the underlying machine's instruction
does. Until recently the C standard was deliberately unclear about
whether arithmetic was ones- or twos-complement. -John]

[...]
> [The history of formal description of programming languages is not
> encouraging. Back in the 1970s the ANSI PL/I standard was defined in
> terms of formal operations on trees, but even so it had bugs/errors.
> Also, per your comment on addition, in a lot of cases the practical
> definition turns into whatever the underlying machine's instruction
> does. Until recently the C standard was deliberately unclear about
> whether arithmetic was ones- or twos-complement. -John]

The C standard still doesn't mandate two's-complement.

The 1990 edition of the C standard was vague about integer
representations, though it did impose some requirements. It required
a "pure binary" representation, and it required, for example,
a value that is within the range of both int and unsigned int to
have the same representation in both. That excluded some of the
more exotic possibilites. (It mentioned 2's complement a few times,
but only as an example.)

The 1999 standard explicitly required one of three representations:
sign and magnitude, two's complement, or one's complement. It also
explicitly permitted padding bits (bits that don't contribute
to the value, and that can either be ignored or create trap
representations).

The 2011 standard corrected the spelling of "ones' complement",
but otherwise didn't change anything significant. (The 2017 edition
was a minor update.)

The upcoming 2023 standard mandates two's complement. And it
requires INT_MIN to be exactly -INT_MAX-1; previously INT_MIN could
be equal to -INT_MAX, and -INT_MAX-1 could be a trap representation.
It still permits padding bits and trap representations.

Note that twos's complement *representation* doesn't imply two's
complement *behavior* on overflow. Signed integer overflow still
has undefined behavior.

--
Keith Thompson (The_Other_Keith) Keith.S.Thompson+u@gmail.com
Working, but not speaking, for XCOM Labs
void Void(void) { Void(); } /* The recursive call of the void */

On Sunday, February 5, 2023 at 6:01:04 PM UTC-8, Keith Thompson wrote:

(snip)

> The upcoming 2023 standard mandates two's complement. And it
> requires INT_MIN to be exactly -INT_MAX-1; previously INT_MIN could
> be equal to -INT_MAX, and -INT_MAX-1 could be a trap representation.
> It still permits padding bits and trap representations.

Too bad for those CDC computers, and Unisys computers.
Last I know of sign-magnitude is the IBM 7090 and 7094.

> Note that twos's complement *representation* doesn't imply two's
> complement *behavior* on overflow. Signed integer overflow still
> has undefined behavior.

Overflow behavior mostly depends on the hardware.

Many computers, such as the IBM S/360 and successors, have a bit that
enables or disables the fixed point overflow exception. (For IBM, it
also applies to decimal overflow.)

For IA32, that is x86, there is the INTO instruction, which is put
after any instruction that could generate overflow, and causes the
interrupt if the overflow bit is set. Compilers would have to generate
that instruction.

It seems, though, that has gone away in x86-64 mode.

I don't know that there is any replacement, other than a conditional
branch based on the overflow flag.

Fortran programmers rely on fixed point overflow, as they have been
doing for 60 years, and don't have unsigned.

(There are two routines in TeX that Knuth suggests replacing with
assembly code. Those do multiply and divide, with 32 bit fixed point
values, 16 bits after the binary point. Pascal has no option for
avoiding the overflow trap, and it takes a lot of Pascal code to do
the multiply and divide!)

On 2/6/23 10:26 PM, gah4 wrote:

> Too bad for those CDC computers, and Unisys computers.
> Last I know of sign-magnitude is the IBM 7090 and 7094.

AFAIK use IEEE-754 floating point numbers still sign-magnitude
representation.
Then the same representation of integral numbers may have advantages in
computations.

DoDi
[I presume the sign-magnitude is to enable the hidden bit trick,
which doesn't apply in unscaled integers. -John]

On Tuesday, February 7, 2023 at 6:30:40 PM UTC-8, Hans-Peter Diettrich wrote:
> On 2/6/23 10:26 PM, gah4 wrote:

> > Too bad for those CDC computers, and Unisys computers.
> > Last I know of sign-magnitude is the IBM 7090 and 7094.

> AFAIK use IEEE-754 floating point numbers still sign-magnitude
> representation.
> Then the same representation of integral numbers may have advantages in
> computations.

> [I presume the sign-magnitude is to enable the hidden bit trick,
> which doesn't apply in unscaled integers. -John]

Yes, I meant integer representation.

Well, I have been wondering for years when we get a C compiler
for the 7090 so we can test out sign-magnitude integers.

I think the 7090 does 16 bit integers, at least that is what
its Fortran compilers did, stored in 36 bit words.

As for floating point, the PDP-10 uses a two's complement
floating point format. It does two's complement on the
whole 36 bit word. The result is that fixed point compare
instructions work on floating point values.
[The 704x/709x series did 36 bit sign-magnitude arithmetic. Fortran
integers were limited to 15 bits plus a sign, probably because that
was the size of addresses, and they expected integer arithmetic to
be used only for counting and subscripts. In 709 Fortran II they
expanded them to 17 bits, in 7090 Fortran IV they were finally a
full word. -John]

Hans-Peter Diettrich <DrDiettrich1@netscape.net> writes:
>AFAIK use IEEE-754 floating point numbers still sign-magnitude
>representation.
>Then the same representation of integral numbers may have advantages in
>computations.

Such as? Anyway, whatever these advantages may be, they have not been
enough to prevent the extermination of sign-magnitude integers.

>[I presume the sign-magnitude is to enable the hidden bit trick,
>which doesn't apply in unscaled integers. -John]

With a ones-complement or two's-complement mantissa the hidden bit
would just have the same sign as the sign bit, so this trick is not
tied to sign-magnitude representation.

Some years ago someone sketched a two's-complement representation for
FP (that also includes the exponent), but I did not quite get the
details. Anyway, I expect that whatever the advantages of that
representation are, they are not enough to justify the transition
cost.

- anton
--
M. Anton Ertl
anton@mips.complang.tuwien.ac.at
http://www.complang.tuwien.ac.at/anton/
[PDP-6/10 floating point was two's complement. As someone else recently noted, that
meant they could use fixed point compare instructions. -John]

On 2/7/23 2:31 PM, Hans-Peter Diettrich wrote:
> On 2/6/23 10:26 PM, gah4 wrote:
>
>> Too bad for those CDC computers, and Unisys computers.
>> Last I know of sign-magnitude is the IBM 7090 and 7094.
>
> AFAIK use IEEE-754 floating point numbers still sign-magnitude
> representation.
> Then the same representation of integral numbers may have advantages in
> computations.
>
> DoDi
> [I presume the sign-magnitude is to enable the hidden bit trick,
> which doesn't apply in unscaled integers. -John]

That's correct, the inprecise representation of FP numbers allows for
such tricks. The hidden bit trick can be used again with the FP
exponents, as I outlined in my Dynamic Floating Point Exponents proposal
<https://figshare.com/articles/preprint/Dynamic_Exponents_for_Floating_Point_Numbers-2022-04-07_pdf/19548187>.

DoDi