[SystemSafety] Number Theorist Fears All Published Math Is Wrong

[Steve Tockey]

Derek, Rod,

“Look at the specification of integer square root that I gave earlier - that doesn't look like a "program" to me - it specifies what is to be computed, but says nothing about how to compute the answer at all.”

Yes. Same for the Internal Rate of Return (IRR) proof I posted yesterday.

The contract is not at all executable, it cannot be considered a (computer) “program” by any reasonable definition of the term. It is not a ‘version’ of the program. The contract is exactly, ‘what needs to be computed’, and nothing about how to compute it. The proof is all about how the chosen compute-it part satisfies the requirements established by the ‘what needs to be computed’ contract part.


— steve


From: systemsafety <systemsafety-bounces at lists.techfak.uni-bielefeld.de<mailto:systemsafety-bounces at lists.techfak.uni-bielefeld.de>> on behalf of Roderick Chapman <rod at proteancode.com<mailto:rod at proteancode.com>>
Date: Wednesday, October 30, 2019 at 7:47 AM
To: "systemsafety at lists.techfak.uni-bielefeld.de<mailto:systemsafety at lists.techfak.uni-bielefeld.de>" <systemsafety at lists.techfak.uni-bielefeld.de<mailto:systemsafety at lists.techfak.uni-bielefeld.de>>
Subject: Re: [SystemSafety] Number Theorist Fears All Published Math Is Wrong

On 30/10/2019 12:45, Derek M Jones wrote:
Claimed "proofs of correctness" (non-trivial or otherwise) are essential
N-version programming, with N=2.

Somebody write a program, and somebody writes another program.
One of the programs is labeled as a specification.

That doesn't ring true with me. The "classic" N-version programming experiments that I am aware of were all about N different implementations of the same specification S using programming languages that were at about the same level of abstraction.

Where I've had the privilege to work with formal specifications, I note that they are both "concise and precise" - being both shorter and more abstract than the eventual (and normally imperative) implementation.  There's also no inference that S has to be complete - it can specify a single important property P which must be true, without going to all the trouble of having to specify the behaviour of everything else that a system might do.

Look at the specification of integer square root that I gave earlier - that doesn't look like a "program" to me - it specifies what is to be computed, but says nothing about how to compute the answer at all.

 - Rod

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20191030/e61099f2/attachment-0001.html>