[SystemSafety] Correctness by Construction

[Peter Bernard Ladkin]

On 2020-07-13 20:29 , andrew at andrewbanks.com wrote:
>
> But surely, at some stage, "Correctness" can only be actually proven by EXECUTING that code on the
> target hardware.
I wasn't answering the question "what does it take to show your code correct, whatever correct means
for you?".

I was answering the question "what do you understand CbyC to mean". My answer, as you observe, is
limited to programming source. I agree, obviously, that CbyC used on source, even if it succeeds, is
insufficient to ensure correctness of the executing code. I also recognise that others (such as PB)
think it includes measures to ensure correctness of the executable. But I want to separate concerns.
Plenty of people really look into the processes of turning HL source into machine code/MC-execution
without claiming they are doing CbyC. Conversely, people claiming they are doing CbyC are not
necessarily spending serious effort into those "lower-level" processes. I separate them. The
distinction is justified no matter what you want to call it.

And of course you can (try to) perform CbyC (in my sense), say you are doing so, and completely mess
it up. Minimally, an assessment is needed to judge if you've done OK.

In any case, as pointed out repeatedly by Michael, no matter how you develop it, hopes of getting
your code to do exactly what is wanted founder on the unspecified relation between how you construe
the world to be and how "the world" really is.

PBL

Prof. Peter Bernard Ladkin, Bielefeld, Germany
Styelfy Bleibgsnd
Tel+msg +49 (0)521 880 7319  www.rvs-bi.de





-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20200713/6d85bd82/attachment.sig>