27 Sep
2014
27 Sep
'14
3:51 p.m.
On 9/27/2014 1:59 PM, Paul Koning wrote:
On Sep 27, 2014, at 4:06 PM, ANDY HOLT<andy.holt at
tesco.net> wrote:
So what was his answer?
which one?
all I can find is Green Hills RTOS at 6+
steve
On Sat,
Sep 27, 2014 at 12:50 AM, Dave G4UGM<dave.g4ugm at gmail.com> wrote:
Dijkstra's key interest was proving program correctness (he was a
mathematician).
All the stated languages had features that made this difficult - if not outright
impossible.
But he didn't have a good answer when I asked him if this didn't just push the
problem back
to the program specification, not to mention the problem that in "the real
world" specifications
received frequent modification.
On reading [Dijkstra's] quotes he sounds very
bitter and twisted about all the
languages in common use in commercial and scientific computing when he wrote
that quote (around 1975 I believe)...
He slates Basic, Cobol, Fortran, APL and PL1..
Because they all sucked, for various reasons. Being in common use
doesn't mean that they're good in any absolute ...
Proof of program correctness is one of those
things that I feel "would be nice, but will /never/
happen for real applications?.
I would have thought so too (and that was after taking his course). Then I
found out about a real-time OS that was evaluated under the Common Criteria security
standards to EAL 7 (the highest level), a year or two ago. Take a look at what the
description for that level says; it?s pretty close to proof of correctness, perhaps the
actual thing. And that was for a commercial product with real world applications.
paul