[SystemSafety] Number Theorist Fears All Published Math Is Wrong

[Roderick Chapman]

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/92a0d07d/attachment-0001.html>