[SystemSafety] C for OSs

[Martyn Thomas]

SFAIK, the iFACTS air traffic control tools were written in SPARK and
run on the bare hardware. Roderick Chapman <rod at proteancode.com> will
have the details.

Martyn


On 06/09/2019 14:34, Robert P. Schaefer wrote:
> The problem is a contradiction in what you want to and how to go about doing it.
>
>  For security, you have to write OS “kernel” code that controls hardware.
>
>  For an OS to be “good”, your kernel code has to be small and fast.
>
>  For reasons of hardware access, you need to write assembly language statements to control hardware,
>
>  The only small fast language that supports embedding assembly by pragma is C, and C is inherently insecure.
>
> I’m willing to entertain the notion that I am wrong, but, per the quote:
>
>  "Very smart people have tried for 50 years, and the solution to the is not reduced to practice."
>
> bob s.
> Haystack Observatory, Westford, MA

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: OpenPGP digital signature
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20190906/3ffce86d/attachment.sig>