[SystemSafety] Critical systems Linux

[Peter Bernard Ladkin]

Olwen,

as I am sure you are aware, it is not the mathematics per se which is important, but whether the
representation in the "formal semantics" has clear counterparts in the real electronics. For
example, most semantics take arithmetic as given, but in fact accurate microprocessor arithmetic is
a complex thing in itself for which Kahan won the Turing Award and Jerry Coonen got his PhD.

On 2018-11-22 15:42 , Olwen Morgan wrote:
> 
> 
> de Millo, R. A., Lipton. R. J, and Perlis, A., J., "Social Processes and Proofs of Theorems and
> Programs", CACM, V22, No.5 May 1979 (.pdf available on the net - just google for it).
> 
> It argues that program proofs will never have the status of proofs in mathematics because acceptance
> of a proof in mathematics depends on publication and acceptance by a relevant community of
> mathematicians. The authors did not see that this would necessarily be the case for program proofs.

(Ah, a blast from the past.) The standard answer is that, unlike in math, it is not the proofs
themselves which need to be assessed, but the dependability of the proof checker.

For example, if you have an SOS semantics for a language, you can implement it in Isabelle proof
rules and, subject to your assessment of Isabelle's dependability and your ability to type-check
your rules, you have a provably-correct semantics engine. That technique was used more than a couple
of decades ago by a student of mine to implement a provably-correct DATR interpreter.

PBL

Prof. Peter Bernard Ladkin, Bielefeld, Germany
MoreInCommon
Je suis Charlie
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/mailman/private/systemsafety/attachments/20181122/0e813c23/attachment.sig>