Re: Dijkstra's Methodology for Secure Systems Development

[Left Right]

Sorry, I really only registered to submit a couple of bugs, but I
couldn't miss the opportunity! Well, you see, there is a very well
known ethical school of thinking which does not think that ethics is
relative (I don't believe that too, but for other reasons). Immanuel
Kant is by far the best known proponent of universal ethics. I also
happen to work on my future thesis, which is about formalization of
ethics (as you would guess, if that's possible to formalize, or, at
least, I believe so, then I also must believe it to be universal). The
examples I like to give in this debate (of course there are other
famous school of ethical thought which disagree with this) is the
example of an elevator, which must implement an ethical program in
order to be considered functional (w/o going into detail, it is
possible to construct an elevator, which will be more efficient than
those we use normally, but it would be perceived as unfair).

To put a brief argument for Kant's view of the problem: he believed
that the right thing to do is to act freely, he also believed that
given the opportunity to act freely everyone would choose the same
strategy. These ideas seemed quite solid at the time, but not so much
any more. The world of philosophy of the day was deterministic and had
very weird concepts of what reality is made of :) Nevertheless, many
adopt his categorical imperative as a moral norm (which I don't think
anyone should, but that's a separate story).

Another great ethical thinker, who believed in universal ethics is
Aristotle. Surprisingly, he has a much better grounded view to offer.
The collection of his view also known in the modern world as teleology
survived a lot of paradigm shifts. (I subscribe to this idea too). It
was mostly advanced by philosophers of Abrahamic religions, and so it
is known in the modern world as Tomis or Aviccenism, but it doesn't
have to be religious in nature. I think it was just comfortable for
religions, which wanted to be universal to have a doctrine, which also
wanted to be universal. Put shortly, the premise of this doctrine is
that it is good to give which is due, and it is bad otherwise. Which,
kind of, transfers the responsibility of answering the question of
what is good to what is due, but, in the same sense as we have logical
system which don't define what is true and what is false (this is
mandatory defined outside the system), and they are still useful.

The counterexamples of ethical thought, where good and bad were
considered relative in one sense or another: of course utilitarianism,
libertarianism. Basically, everything that has nowadays to do with the
humaism of the Western world thrives on an assumption that ethics are
relative, perhaps to an individual, maybe to a group, or maybe the
time dimension makes them relative - depends on what philosopher you
pick.

----

I also read the OP, and, I think that there are thoughts that could be
useful, but it is unhelpful that the reaction creates a conflicting
situation. I would suggest the following proposition to Ian Grant, I
think it may be helpful:

It is possible to build a good, solid mathematical model (and it seems
like you are into that kind of programming, since you mention Dijkstra
and Milner very often), but it will not map well to the actual
observed phenomena. This is very well known problem in areas like
molecular biology, particle physics and economics / social studies.
I.e. for example, it is possible to come up with a model, which, given
some input DNA will make interesting inferences about it, but will be
completely worthless for making predictions about how actual ribosomes
synthesize polypeptides. Quite similarly, the hypothesis suggested by
Milner, I think it was "properly typed programs can't be buggy"
appears not to hold water. It is a good, consistent, even solid
theory, but it doesn't capture the nature of programming. And it
doesn't deliver on the promise. Programs in ML, too, have bugs.
I don't say this to discourage you, I think that searching for this
kind of models is important. I just wanted to say that maybe your
conclusions have been premature and lacking the statistical evidence
(lack of evidence isn't in itself a proof of the contrary).

Best,

Oleg