What is a Screen, Really?

Posted to:

    http://lists.gnu.org/archive/html/guile-devel/2014-09/msg00145.html

> But it would nice to get some new major features. Screen is old.. 27 years
> is heck a lot of time. What about the next 27 years? ;)

As far as its apparent functionality goes, GNU screen is one of the best pieces of GNU software I know: there is an unmistakably twisted sort of genius to what it does. But what I only discovered a week or so ago is that Screen is actually only one quarter of an idea that is now over 45 years old. This suggests that what to do over the next 27 years is to implement at least another quarter of it :-)

Here is what I claim is the original expression of Screen, which was called "the message interpreter":

At level 2 we find the "message interpreter" taking care of the allocation of the console keyboard via which conversations between the operator and any of the higher level processes can be carried out. The message interpreter works in close synchronism with the operator. When the operator presses a key, a character is sent to the machine together with an interrupt signal to announce the next keyboard character, whereas the actual printing is done through an output command generated by the machine under control of the message interpreter. (As far as the hardware is concerned the console teleprinter is regarded as two independent peripherals: an input keyboard and an output printer.) If one of the processes opens a conversation, it identifies itself in the opening sentence of the conversation for the benefit of the operator. If, however, the operator opens a conversation, he must identify the process he is addressing, in the opening sentence of the conversation, i.e. this opening sentence must be interpreted before it is known to which of the processes the conversation  is addressed! Here lies the logical reason for the introduction  of a separate sequential process for the console teleprinter, a reason that is reflected in its name, "message interpreter."

Above level 2 it is as if each process had its private  conversational console. The fact that they share the same physical console is translated into a resource restriction of the form "only one conversation at a time," a restriction that is satisfied via mutual synchronization. At this level the next abstraction has been implemented; at higher levels the actual console teleprinter loses its identity. (If the message interpreter had not been on a higher level than the segment controller, then the only way to implement it would have been to make a permanent reservation in core for it; as the conversational vocabulary might become large (as soon as our operators wish to be addressed in fancy messages), this would result in too heavy a permanent demand upon core storage. Therefore, the vocabulary in which the messages are expressed is stored on segments, i.e. as information units that can reside on the drum as well. For this reason the message interpreter is one level higher than the segment controller.)

http://www.cs.utexas.edu/users/EWD/ewd01xx/EWD196.PDF

The other layers of the THE multiprogramming system were equally radical, and still I think there are many people who interpret these ideas in terms of what they already know, and in so doing, they miss the point completely, which is that there is a core methodology that is being _mechanically unfolded_ into a whole coherent design for what we nowadays think of as "an operating system kernel." But modern kernels do not have this economy of principles: witness the insanity
that the Linux kernel device driver stack has mutated into!

When you read this, think of the sequential processes not as "processes" as we know them, but as "processors" or "virtual machines". And don't think of segments and pages in terms of segmented memory models with virtual page maps and swap space, think of them as a kind of storage area network.

So I think we should implement GNU Screen, layers 0 and 1 in addition to layers 2 and 3.

Bankers

Ten of the world’s leading banks have racked up fines and similar "conduct costs" of nearly £150 billion over a period of just five years.

Teaching Men how to Bank

"The Banker's Algorithm derives its name from the fact that this algorithm could be used by the banking system to ensure that no bank ever exceeds its reserves, because a bank would never allocate its reserves in such a way that it could no longer honor all of its debts to its customers. By using the Banker's algorithm, any bank could effectively ensure that whenever customers withdraw their money, the bank never leaves a known "safe-state." If the customer's withdrawal request can be honored without causing the bank to leave the safe state, their request is granted immediately, otherwise they must wait until another customer deposits enough to cover the safe-state deficit."

    http://www.cs.utexas.edu/users/EWD/ewd06xx/EWD623.PDF

Subverting the Laws of Physics

This is a reply to:

   http://lists.gnu.org/archive/html/guile-devel/2014-09/msg00124.html

> How can we know that the enemy isn't using some laws of physics that
> we weren't taught at school (and that he deliberately keeps that
> knowledge out of schools)?

This was probably meant as a facetious comment, but with what is for
good reason called "the devil's luck," you've hit the proverbial nail
right on the head. The law of physics that the enemy is using, the
knowledge of which he keeps out of schools (and universities), is the
law that says every measurement necessarily must have a physical
meaning, and that the meaning of any empirical measurement is always
in the context of the meaning of other empirical measurements: no
experimental measurement has an absolute meaning. And you will see
this as soon as you consider, on the one hand, what is the meaning of
a reading of a P.D. of "1 V" on a meter, and on the other hand, what
is the meaning of "1 MeV" as the energy of a particle in an
accelerator ring.  Eventually, the semantics of any physical
measurement boil down to one or more of the defined reference units in
some metric system such as the Système international d'unités or
S.I., where the fundamental units are seconds, metres, kilograms,
amperes etc.

The science of metrology is all of the knowledge people have as to
how to go about actually making measurements in terms of these defined
units: how to calibrate devices, which methods are the most accurate,
etc. And the metrologists who work in the various national institutes
of weights and measures around the world use various precisely
specified experimental methods to construct the reference data, called
"realizations of the units," by which people in that place calibrate
measurements.  So the actual measurements that any laboratory makes
are always determined by a complex body of physical theory.

For example, the second may be defined as a certain number of
oscillations of an ion at a certain temperature in a caesium fountain
clock. Now, in order to know what this means, you need to know exactly how and why a caesium fountain clock actually works. So the
accurate measurement of a one second interval embodies (and therefore
depends upon) a great deal of sophisticated theory about how caesium
atoms behave at very low temperatures. And, as I'm sure Oleg would be
able to explain to you, if you know this, then you know that a
measurement of "one second" or "one meter" is by no means an immediate
observation: it is an elaborate series of inferences from other
measurements of other units all defined in the same system.

But this detail is not taught in schools, and it doesn't seem to
figure much in pop-science "literature" either. Perhaps this is
because it is a technical subject, and it is thought that one can't
teach people what a second really is until one has taught them how a
caesium fountain clock works. Or it may be because, in a sense, these
details are arbitrary: the idea of physical relativity in its most
general form is that of a "gauge theory" where the results of local
physical measurements are assumed to be globally consistent, under a
mapping which takes the results of local measurements from one region
to a neighbouring one. This mapping is called the local gauge
transformation. Then if the idea of a gauge theory is consistent
(which, a priori, is by no means necessary) it won't matter what the
local gauge at any point actually is, in the sense that the
"objective" physics is supposed to be an invariant of the
transformations from one local gauge to the next.  So it may be that
because the particular set of experimental methods (the
realizations) used to establish the reference data in any particular
gauge are arbitrary, people don't see any need to teach any of them.

Or it could be for the disingenuous reason that teaching this would
seem to undermine the "authority" and the "objectivity" of scientific
knowledge, and thereby leave room for the idea that God is in fact the
origin of all actual Human knowledge.

Whatever the reasons, the units of measurement are more often than not
presented to physics students as being in some sense "absolute" or
"god given ('because the professor said so!')". But they are defined in
the S.I., or some moral equivalent of it, so for better or for worse,
the S.I. and the c.g.s. systems, taken together, are effectively "the
denotational semantics of physical measurement." It's a pity though
that so many people who, because they write books about it, seem
to think they know physics, don't seem to actually know how any
physical measurements are made in practice.

The relevance of all this is that what I am proposing is an analogous
method of defining the semantics of programming languages: instead of
taking them as 'absolute' in terms of "whatever the compiler binary
and the CPU actually does with my source code," (the analogue of "what
The Professor says they are") we define them in terms of some formally
specified, and therefore well-known, "standard interpretations."
Precisely what these are doesn't actually matter: as long as they are
complete, machine readable and well understood, then, provided we know
what we're talking about, we will be able to make the necessary
"gauge transformations" between any two different interpretations, by
defining translators of the semantics in one form to the other, and
vice versa. And the mutual coherence of these different
interpretations will be the actual knowledge we have that the
semantics we think we know are what we actually think they are.
This state of knowledge is what I call a semantic fixed-point.

This is very different to a syntactic fixed-point, where we simply
compare the forms of the representations that appear in a terminal
window (or in documentation on a web page, for pity's sake!)  and
assume we know the semantics, without actually having any evidence
whether or not that assumption is correct. It is analogous to the
difference between, on the one hand, doing a physical experiment
twice, using two substantially different metric systems and comparing
the results 'metrologically', by converting between the different
realizations of units; and on the other hand, simply doing the
experiment once, using whatever is the conventional metric system, and
'blindly' reading the results directly off the calibrated scales on
the instruments.

> Then our enemy will always be in control! 

Only whilst the only place that people actually learn anything is in
school, and I hope that nobody still reading this actually believes
that. Formal education is only a "first-stage bootstrap": at
school/university we need just to learn enough from our teachers to be
able to continue learning independently.

The root of the problem, at least in so far as the education system is
concerned, is that this first-stage bootstrap has an "initialization
trap door" in it. The single most important thing one needs to teach
students, if they are to continue learning under their own steam, is
this: "we only ever actually know something when we know how and
why it is that we know that thing." And it is the almost total
failure to effectively teach this which gives the game away. The
evidence I have that this is not taught (i.e. the reasons I think that
I actually know this to be the case) are the countless instances I
see where people mindlessly assert "facts" which they "know," but
cannot explain how it is that they actually know these things. For
example, when someone asserts: "Then our enemy will always be in
control!" as if this were an immediate consequence of the fact that
the enemy controls what is taught in schools.

> This reasoning, although paranoid, seems completely valid [...]

Many teachers and lecturers don't themselves know this fundamental
epistemological principle, so the conspiracy is to a large extent
self-perpetuating, and need not even be a conscious one. But because
the subject is fundamentally based on epistemology and logic, I think
it more likely than not that it is a conscious conspiracy in computer
science, as it is taught in "prestigious" universities in Britain, the
USA and other countries where English is widely spoken.

To decide whether or not this is "paranoid reasoning" we can consider
"means, motive and opportunity." Such institutions as these are
typically considered to be "leading research in the field," and so
they have a great deal of autonomy in the choice of what they
teach. They also rely on foreign students for a significant part of
their income, and they exploit this source, ravenously and more or
less indiscriminately. So to prevent the dissemination of "valuable
knowledge" too far and wide (which, besides putting it in the hands of
"the enemy", would also erode their advantage, and thereby undermine
their ability to exploit foreign students), they intentionally
dumb-down the exoteric computer science syllabus.

The systemic nature of this conspiracy theory is not very different
from the dumbing-down mechanism which is evident in the mass media,
and which Chomsky calls "Manufacturing Consent."  The argument I've
just made proves nothing of necessity, but it demonstrates
possibility, and since paranoia is an unfounded fear of persecution,
it needs to be shown to be invalid before the assertion, that there
has been a conscious effort, by some people, to dumb-down the study of
logic and computer science in certain universities, could justifiably
be claimed to be "paranoid reasoning".

> [...] but it does abuse the notion of "enemy", by putting it in an
> extremely asymmetical situation.

Have you not seen either episode IV of "Star Wars", or "Matrix:
Revolutions", or "The Fifth Element", or "Kill Bill", or "The Bourne
Ultimatum", or "Salt", or "Avatar", or "Transcendence" for that
matter? These all "abuse the notion of 'enemy'" in exactly that way.

Finally, you seem to need to be told that nobody who had studied
computer science at any sort of university, anywhere in the world,
could possibly have come up with anything quite so stupifyingly
insightful as you did when you wrote "... we could detect that by
generating all possible binary sequences and checking whether the
generated ones are the same as the viewed ones. Or could this process
also be sabotaged?"

That, my friend, is the sort of thinking that could one day earn you
a PhD in Economics, or Theoretical Physics, or maybe even a job
interview at a nondescript office-block just outside of McLean, VA, a
prelude to a long and distinguished career as a government-sponsored
under-cover WikipediA editor. So you have a great future ahead of you;
provided that is, you never set foot in the theater.

Happy WikipediA hacking.

Ian

The Free, the Fair and the Forged

Paul Koning <paulkoning@comcast.net> writes:

> First of all, for the reasons I mentioned yesterday, it doesn’t
> really have anything to do with voting machines.  The issue with
> voting machines is not the trustworthiness of programmers or the
> reliability of their work.  It is the fact that paperless machines
> are conceptually defective, and that defect would remain even if the
> programmers were infallible angels.

The whole problem with Karger-Schell trap doors (see
http://seclab.cs.ucdavis.edu/projects/history/papers/karg74.pdf page
51) is that even if programmers were actually known to _be_
infallible angels, the software they produce would not be trustworthy.

> A voting system — i.e., the entire legal, social, and mechanical
> machinery and processes involved in running an election — is valid
> only if (a) it is sufficiently honest, and (b) that honesty can be
> confirmed by ANY fair observer with near-average intellectual
> abilities.  For (b), if John Doe the farmer or Fred Flintstone the
> day laborer can’t be a poll watcher and see for himself that the
> polls are honest, you don’t have a reliable election.

For the purposes of this discussion, can we assume that (b) implies
(a), or can I raise the paranoia level a notch, and consider the
possibility that there is a Karger-Schell "compiler" trap door in the
education system? This would mean we could have a problem, because it
might be that what John Doe and Fred Flintstone _actually know_ is
honest, is inconsistent with what educated people judge as honest,
with respect to your (a).

I am serious. We _can_ discuss this. If you want to muse over it
yourself a little, start by thinking of a teacher as a sort of
compiler, taking source from text books and compiling some 'object
code' which is the mind of her student. c.f. Dijkstra's comment "I
long ago became convinced that the only students to whom I could teach
anything would become misfits." I think I read this in:

  http://www.cs.utexas.edu/users/EWD/misc/vanVlissingenInterview.html

So, did Dijkstra ever teach you anything? If so, then my
commiserations, but "welcome to the misfits club!" I am pretty sure
Roger is a member, and John Harrison too, so the misfits seem to be
doing OK, as long as you don't count me.

I think a better criterion by which to judge what is a free and fair
election is to let the populace as a whole decide that _after the
election_. And if it is not judged free and fair, then the election is
repeated. And so on and so forth, until the whole population is in
unanimous agreement. Then it doesn't matter if there are trap doors in
the voting hardware and in the software, because they will show up
like any other device malfunction would. So the manufacturer would
have to replace the failing components of the system. And if the
replacements also failed, then they would have to be replaced. So the
manufacturer of voting machines which corrupt the data they collect
will not be in business for very long.  And I think that the business
of any Government elected like this will likely be far far more
efficient and far more easily seen to be for the greater good, and not
solely in the interests of some "powerful" minority.

> Paper ballots, with some straightforward precautions, pass
> these tests.

One needs to take into the account the whole process though. In a
general election in a country the size of the United States of
America, the organization necessary to carry out a paper ballot is
enormous. It may be that a few individuals can be poll-watchers, and
can directly verify the counts of paper votes, and know to some extent
that the actual votes those counts represent exist, and are all the
votes that were made. But then only a few people are actual
witnesses. What these people do is to produce a certificate of some
sort. They sign a paper saying "I observed the electoral process at
polling station #nnn on this date dd/mm/yy, and I hereby declare it to
have been conducted in a free and fair manner."  Then all these papers
have to be collected up and at some point authenticated. And of course
all the direct evidence has to be collected too: the data that says "I
hereby certify that Box mmm, sealed at polling station nnn, on date
dd/mm/yy hh:mm, contains the following: x for canditate X, y for
candidate Y, z spoiled." And this data has to be authenticated and
collected. And the process is a distributed one. So at some point the
data has to be collated and summarized. And _that_ process too has to
be verified. At various levels people are using computers, electronic
communications systems etc.

What I am trying to say is that a paper ballot is _almost_ an
electronic one. The only part that's different is the actual act of
voting. But that is not infallible either. The authenticity of the
electoral roll has to be checked to make sure there aren't false
entries that can be 'filled in' by someone who knows which are the
false numbers on the register, and the individual id's of voters have
to be checked, etc, etc. Thus the integrity of the people who check
these things must checked, etc, etc.

And the question I have for anyone that says a paper ballot can be
made verifiably free and fair is "Who makes the judgement that the
whole combined process is free and fair, and on what basis do they
make that judgement? (i.e. in the words of Martin-Lof, what is it that
they must _actually know_ in order to have the right to say this?)"

> Computerized machinery of ANY kind, whether closed (Diebold)
> or open source, are utterly incapable of providing a
> legitimate election system. 

In order to know this, you need to know the _reasons why_ it is
incapable. So you need to be able to give an informal proof showing
that there is some fundamental difference between paper ballots
and electronic ballots which makes the latter incapable of being
verifiably fair where the former are.

> But while lack of trust in the software developers only makes
> it worse (which is why I mentioned Diebold as a particular
> offender), the presence of trust along the lines you discuss
> does not cure the problem.  It might possibly convince you
> and me (though the odds of convincing me are quite low)
> — it won’t and can’t convince John Doe the farmer, and until
> you can do that the election does not have legitimacy.

This means I didn't explain the idea properly. I was not expecting the
public to be able to verify the code and the hardware in the
electronic vote machine, I was expecting the process as a whole to be
verifiable, tying the individual items of data together with actual
knowledge of how the whole system is arranged.

Perhaps I can give a less vague idea by example. I think we could make
electronic voting systems verifiable in this way if the voter gave a
certificate of authentication to the machine. Imagine that in each
booth there's a numeric key-pad and a die, and each voter, in secret,
generates a 10 digit random number which is the voting machine's
certificate of authenticity of the vote that person cast. The machine
records and reports the anonymous certificate and the vote together
with the date, time, polling station id, etc. The voter may also
record the details, if they wish to (and they will be encouraged to do
so,) or they can choose to have it appear on a printed paper receipt
that the machine produces, and they will be asked to verify that what
is printed is correct, and that fact will also be recorded. Regardless
of whether they choose to record their random number or not, the
receipt will include the polling station details, the date and time
and the serial number of the machine.  Then when the results of the
election as a whole are posted, a cryptographic hash of each secret
number appended to that person's vote is published, along with the
hash algorithm (the algorithm is chosen at random, after all the votes
have been collected). Individuals can compute by a published
algorithm, what number should appear in the published list, which will
show that their vote was accurately represented in the election. So
individually, people will know that their votes are there, and if they
aren't they have a certificate that proves this is the case, and they
can protest.  This certificate ought to appear at various points in
the audit trail of the electoral processing that leads from the voting
machine to the final published result. This will make it easier to
locate failures.

The final stage of the election requires voters to confirm that their
vote has been accurately represented: this is done by transmitting the
random number to the electoral registrar, by some means of their
choice. It could be via a web site, a text message or some such. At
that point another hash of the random number and their vote appended
to the vote sequence number on the receipt they got from the machine
is published. Then the count is done to determine the result. They
will then be able to see the fact that their vote was counted
correctly by calculating the second hash function on their random key
and the machine receipt no and their voting choice. If the number they
get isn't listed, then they will protest.

There would hopefully be a very wide choice of means to do the
calculation of hash functions. People could write their own programs,
or use government-supplied programs; and they will be able to compare
the results these different systems give. So they can individually
know that their own vote was very probably correctly represented in
the count.

Regardless of the specific problems you might see in this scheme (and
they will be many) I hope I've explained the general principle of
macro-verifying the wole process, rather than trying to micro-verify
each and every one of the individual steps. The principle is that if
we do this 'big step' verification, then we can simply assume the
'small step' semantics are good, because otherwise the system would
fail; and this would either show up as a failure at the high-level
verification, or if not, we would have found a way to make a 10
peta-qubit quantum computer, so either way, we win.

> Second observation: you raise some interesting questions.  I gather
> from your email that you’re hoping for actions, but I can’t tell
> from the essay what actions you’re looking for.  Are you looking for
> the open source community to adopt more rigor in design? 
> What do you view as next steps, what would you define as a
> successful outcome?

Yes, all software, not just open source, will be produced with rigour:
specifically, that rigour will be achieved by only using software that
is machine generated from a formal specification. I don't mean
anything especially mathematical-looking. Take an assembler, for
example. Imagine you are rewriting the disaster that is GNU
as. Instead of writing thousands of lines of C full of macros and
what-not, you write a grammar for a language which specifies the
syntax of assembler statements, and their semantics, which are the
rules for encoding instructions into macine code when given abstract
syntax trees representing the instruction and its arguments. You spend
nine months doing this, and in the next three months you write a
parser for that language, and you write the data files that describe
the instruction encoding rules for the different CPUs such as i386,
PowerPC etc. These you are just transliterations of the manufacturer's
documentation for the CPU instruction set.

Then you define another language which defines a process which takes
abstract syntax trees representing these CPU metadata files, and
generates source code to implement the assembler in some concrete
language. Then you write a translator for C, say. You could also write
another translation which generates Python code from the same formal
specification, and then you would have an assembler written in Python
which was 100% compatible with the C one. Now because these concrete
source-code implementations in C and Python are automatically
generated, you can be sure that there are no "extraneous semantics" in
them, because there is not one single line of code in there that does
not have just one purpose, being the implementation of that part of
the specification that caused it to be generated.

And then, if you wanted to, you could implement the i386 assembler in
Z80 assembler, and the Z80 assembler in PDP11 assembler. This would
just be a matter of writing different translations of the abstract
assembler specs, instead of producing C or Python, they produce PDP11
or Z80 assembler code. Then you could go out to the garage and fire up
your old PDP11 to compile the i386 assembler into Z80 machine code,
and transfer the data via an RS232 cable to your Z80 development
board. Then you wire up the development board to the USB serial
adapter on your fancy new 8 processor xxxx server, and use the Z80
development board as a trusted hardware platform from which you can
reflash the BIOS with your specialized boot loader, which boots
directly off the xxxx storage area network, rather than a local IDE
hard disk drive, because you really have no idea what that's got on
it.

Now this process will give you confidence in that machine, but your
customers won't have any basis for extra confidence, unless you
publish the method and the formal semantics you used. Then one of them
could carry out a similar exercise, using an IBM 370 and an Apple ][e
with a 3270 terminal adapter. It wouldn't be so much work for them,
they'd just need to program the translators to 370 assembler and 6502.

So this is not merely a certificate that xxxx be offering, it is the
possibility of actually knowing that the system is secure. And I think
you'd sell more machines if you did that.

> Are you looking to "find a way to re-employ all the people
> who enjoy coding”?

The people who enjoy coding will have to be trained to think on a
higer level. Instead of thinking about just one program they're
working on, they'll have to learn to generalise that technology, so
that they will be thinking about an entire generic class of programs
implementing that type of system, and using what Roger Schell calls
"local configuration data" to adapt the specification to specific
conditions in a given concrete implementation. The local configuration
would be written in a language designed for exactly this purpose, so
that it cannot be used to introduce "extraneous semantics".

> [...] what would you define as a successful outcome?

The successful outcome will be when all governments spend twice as
much on education as they currently spend on the military, and when
military service is known by all to be a necessary and just part of
education.

---

> Third: reading between the lines, I think you’re saying that the
> formal statement of the algorithm’s properties (its pre- and
> post-conditions) are actually equivalent to the algorithm, and one is
> no easier or harder to produce than the other (there’s a more or less
> mechanical mapping from one to the other).  I agree with that.  The
> corrolary is that anyone willing and able to produce the one is
> capable of producing the other.  Or in other words, the reason that
> you see little of this (outside the world of people building seriously
> secure systems) is that few programmers are either willing or,
> especially, able.

Yes. I hope that the only part of that you had to read from between
the lines was the bit about few programmers being able to do it. This
is not news though. Roger tells several good stories about it from
the early 60s in the Computer Security History Project interview.

> I was going to say that part of the program is that people program
> in languages that are unsuitable for constructing reliable systems,
> such as C or C++.  But that’s not quite true.  Consider that Dijstra
> did his early work in assembly language, which is a bit worse than
> even C.

My experience is that assembler is actually much better when you are
generating code automatically from a formal spec. You can compose
fragments of assembler programmatically from a machine readable formal
spec. much more easily than you can fragments of C, where you have to
worry about large-scale structure, declaring variables and
what-not. When you do this with assembler, all you need to worry about
is register allocation, and I think it very likely there are ways to
automate that.

> What probably is accurate is to say that the right choice
> will make it easier, or will help compensate for less than complete
> rigor.  For example, a lot of software developers use design specs
> of varying levels of detail and formalism.  Few are the kinds of
> formal specifications Dijkstra talked about.  And as such, they
> don’t produce the same benefits, but they do produce *some*
> benefit. And for such intermediate levels of rigor, using good tools
> helps.  Implement a moderately precise spec using C, or using Ada or
> Modula-3 — the resulting product quality will most likely be lower
> in the C implementation.

I think I agree, but I am suggesting using even better tools than
general-purpose programming languages. The problem with Ada and
Modula-3 etc. is that they are _too_ flexible. You have no way to
verify that what the programmer wrote only does what it is supposed to
do, so you can't know that "... there is no extraneous code and the
system is shown to do what it supposed to do – _and nothing more._"
(Anderson et al. "Subversion as a Threat in Information Warfare")

It is better to use a domain-specific language, with a formal
semantics, so that you can generate concrete code in any
language. Your abstract system, the one written in the domain-specific
language, is then immune to subversion by any particular compiler or
system.

> On specifications, rigorous analysis, and security: are you familiar
> with the international standard for security evaluation called
> Common Criteria?  I’ve been involved in applying that process to our
> products for some time now.  Rhere are 7 levels, we’re using level 2
> which appears to be quite common, though some of our other products
> use level 4.  Even at level 2 it has visible benefits.  I recently
> heard of a real-time OS that had been evaluated to level 7.  Pretty
> amazing; that requires full formal specifications and analysis.  Hm,
> that suggests that the sort of thing that Dijkstra was talking about
> is indeed used today in commercial practice — even if only rarely.

I didn't know about the ISO secure systems standard until I read about
them in the aforementioned Anderson et. al., which Roger Schell
pointed us to. They seem to be a successor to the Orange Book TCSEC. I
have scanned them (after spending an hour or so making a mental map of
the acronyms!) I need to spend at least another 100 hours before I
could say I know what it's about! The problem with _all_ the ISO
standards is that they're written in English, for people to read. I
want the ISO to join in with this project I am trying to describe, and
produce machine-readable documents which contain all the data in the
standards, so that people can write parsers to read the languages the
data is defined in, and then write programs to translate that ISO spec
into a reference implementation. This is not as hard as you might
think. Already the ISO C standard includes a grammar, which is BNF
which you can just type into a YACC parser spec. and generate a set of
parsing tables in Moscow ML, say. So I wrote an ISO 1989 C parser in a
very little time. But there is a lot more to C than the parser. The C
grammar doesn't constrain parsed code to those programs which have
well-defined semantics. There are lots of extra conditions which are
written informally in the language spec, (at least in the freely
available drafts which I have seen. Maybe if you have the published
standards you have access to more.) And these have to be checked in a
separate stage.

This too could be formalised though. I have been experimenting with a
very simple term-rewriting language in which the semantic phases of a
C compiler could be formally described. It's just a bottom-up pattern
matching and term-rewriting notation, and using this I can express
quite a lot of the post-parsing 'semantics' in the C spec.  I wrote an
interpreter for this term-rewriting language in a few hundred lines of
Standard ML, and I think anyone could do something similar in any
other general-purpose programming language. So if the ISO standard
came with the machine-readable semantics of a reference
implementation, then anyone could independently produce a reference C
compiler, which they could use to compile an open source C compiler,
whose source code they have thoroughly audited.

The code for this is at the github repo I sent you a link to. The file
that has it is src/dynlibs/ffi/testrewrite.sml

> A few of your examples seem to be inaccurate.  The one about
> paper money has not been valid for a century (no money in
> current use is backed by anything).

I know. But why do you say that makes my example invalid?  The fact
that the vast majority of USD, GBP and very probably many, many other
promisory notes in circulation, are forged doesn't mean this is not a
valid example of forgery of a certificate! Arguably it is a better
example, because you can just look in your bill-fold if you want to
see it for yourself! The note represents a promise, and the number on
the note is a certificate of the trustworthiness of the promise. But
most people think the note itself has value, which is how the forgers
managed to get away with it so long; that and the fact that the
forgers are the same people who produce the genuine notes, so the
forgeries can be made physically just as convincing as the real
things.

If there _is_ some knowledge which discriminates the forged notes from
the genuine ones then it will show up in their 'street value'. So you
might want to try to withdraw your USD 100,000 savings in US$ 2 bills,
for example, and if they said "Certainly Sir, that will be $US
10,000,000 then you know you're onto something :-) If it doesn't work
with $2 then try another denomination.

But if the authenticity of the certificate is not simply encoded in
the denominations, well then you're out of luck. It could be an
arbitrarily complex sub-set of the serial numbers, and without the
actual algorithm for checking them (which is a one-way function, one
would hope, otherwise they screwed-up disastrously!) you won't be able
to know.  Whatever it is, if there is such a "Federal reserve-reserve
currency," it must have been enshrined in Federal law somewhere. So
the only people who would know about it would be people who know
enough to be able understand the statutes in detail. I.e. people who
have been to a "really good" law school, and had a "really good"
teacher, and who weren't "the wrong sort of person," which is a
euphemism for someone who shows any sign whatsoever of moral or
intellectual integrity. I am now wondering if maybe I know more about
conservative American domestic politics than I thought I did. :-)

> A more significant one -- you said: "This is why NOBODY really
> understands public-key cryptography algorithms: because no-one
> actually knows WHY they are secure.”  That’s not right.  Public key
> algorithms, especially RSA, are quite simple.  RSA is simpler than
> FFT, I would say.  It is entirely obvious that they are NOT
> absolutely secure.  It is also entirely obvious that RSA is NO MORE
> secure than the difficulty of factoring a number of a given size.
> (Some crypto systems — but, as far as I recall, not RSA — have
> proofs of security that demonstrates they are AS secure as a certain
> hard math problem, rather than only being at most as secure as
> that.)  The practical usefulness of RSA derives simply from two
> facts: (a) the best known factoring algorithm is hard enough that
> factoring a 2000 bit number is unaffordable, and (b) there are no
> known attacks on RSA that are easier than factoring.  It’s really as
> simple as that.

Someone must have changed the text in transmission, because the rest
of my paragraph, the first sentence of which you quoted above, says
pretty much what you are saying. The knowledge that the PK certifies
is not actual knowledge of security, it is simply the absence of
actual knowledge that it is not secure. I.e. it is the absence of a
computationally feasible algorithm for computing the inverse of the
'one-way' function. The mathematics is only involved in computing the
values of the function, or showing, say, that the factorization
problem reduces to the problem in question. There is never any
mathematics _per se_ involved in the deduction that the inverse of the
one-way function is computationally infeasible, because that requires
knowing enough about every single one of the possible algorithms there
are which compute it, to show that they are all exponential in time.

So the security of the algorithm is not known, it is just the
INSECURITY of the algorithm is ASSUMED to be UNKNOWN. Now that might
be OK, if there were plausible grounds for the assumption being a
valid one. But there aren't any. There are however plausible grounds
for the assumption being INVALID, because if someone did know a way to
crack a popular PK cryptographic code then it is more likely that they
would keep that secret to themselves, than that they would publish
it. This evaluation of the probability being > 50% comes from the fact
that we are dealing with a situation in which the adversary is assumed
to have some motive to intercept and decipher encryted messages, so it
seems they would be more likely not to tell you that they can do this;
and it seems reasonable to assume that the adversary will take every
opportunity to make it easier for them to decrypt your messages. But
these days, not all adversaries are reasonable, so who knows!

Either way, anyone who claims PK cryptography is in any sense
positively secure is obliged to explain why what I have said here is
invalid. Your (a) and (b) may _seem_ to be statements about what is
known. But that is not what is _actually known_. What is _actually
known_ in general is utterly unknowable to any one of us. Your (a) and
(b) are only hypotheses about what is not known _in general,_ and I
hope I've explained why I think their truth is implausible.

>  (By the way, (a) becomes false as soon as quantum
> computers become feasible at that scale; factoring is fast in
> quantum computers if only you could build one bigger than a few
> dozen qubits.)  The same sort of statement of practical strength
> applies to all cryptosystems with the single exception of One Time
> Pad (which is easily proven to be unconditionally secure).  For a
> lot more in a reasonably easy to read package, I recommend “Applied
> Cryptography” by Bruce Scheier.

I've heard of Schneier's book, and his blog, but I've not read
anything of his. If he doesn't mention this issue of the absence of
actual knowledge though, then I don't feel particularly inclined to go
out of my way to read it.

I was a Unix system administrator for about 15 years, and the issue I
constantly came up against with security is that it is _always_ a
question of actual knowledge, and that the necessary actual knowledge
almost _never_ existed. So my conclusion was that computer and
communications security was an emotional state, not an intellectual
one. You can spend months locking down all the potential problems in a
system, and as a result of all that work you feel safe and secure. And
then a vulnerability is publicly announced, concerning some critical
component in your system and *poof*, all that security is vaporised!
In an instant. Yet that vulnerability was there all the time you felt
safe and secure. So the cause of that all-important sense of security
is not knowledge, it's ignorance.

Because of this, quite early on I began thinking about security from
the point of view of it being what George Bush Jr. memorably referred
to as an "unknown unknown" as opposed to a "known unknown", and I
would _assume_ that there was always at least one compromised user
account on each machine on the network, and that the root account on
one or more of the central servers was compromised. And I hope I had
that in mind when I made decisions about how to configure things.

But what I am proposing is a method that will allow us to base
security on actual knowledge rather than emotion. All we need to do is
learn how to generate code automatically, and how to calculate with
probabilities.

> On Sep 19, 2014, at 9:18 PM, Ian Grant <ian.a.n.grant@googlemail.com> wrote:
> > ...
> > What do you think are your chances of persuading xxxxxxx to give
> > your three best programmers a one-year sabbatical, to re-juvinate
> > their careers, and show the world that xxxx can produce world-class
> > software like those Idaho moo-cows of his produce milk?

> On that notion: I like it, but I don’t think the odds are good.
> xxxx is much more a PC hardware company.  The business I’m in is
> storage systems, that has a large software component.  And there are
> other parts that are all software.  Still, I’m not sure how the sort
> of idea you mention would fly.

Discussing it can't do any harm, can it? Storage systems are just
layers 0 and 1 of the THE-mps, you needn't implement layers 2 and 3 if
you don't want to.  And I gave the example above of one selling point:
real security. I'm not aware that anyone offers that these days, or if
they do it must be at a price that's out of my ability to even
imagine. You could use this as a basis for that level 7 validation for
your storage products. I would be happy to help in way I can, and
Roger knows the methodology, because he has used it, probably many,
many times, so I'm sure Aesec would be able to help too. I do not have
any connection with that company; my only interest in your doing this
is that I would like to be able to source hardware that is potentially
knowably secure, so I am going to encourage all hardware manufacturers
to do this.

Thank you very, very much for your comments. I can't tell you how good
it is to be able to discuss these things openly with someone who goes
to some trouble to read and understand what I have written.

Best wishes,
Ian

How to Write Programs

Thesis: The Software Development Process Itself is THE Major Security
Vulnerability in Current Computing and Communications Practices

This is because feasibility of the process depends entirely on re-use
of concrete implementations of algorithms, and so software developers
must routinely download and run code, because it is absolutely
necessary if they are to do their work. The quantity of code that they
download and run is far, far greater than they could possibly inspect,
even cursorily. Therefore software developers are constantly running
unknown code. Any such code they run as part of their work typically
has both read and write access to all the other code they work on,
because they typically use the same machine user account for all their
work. On Unix systems, this is practically mandated by the fact that
account setups are not easy to duplicate, and switching from one
account to another is not easy, because it is almost impossible to
transfer the 'desktop' setups and running applications from one user
account to another, without stopping and restarting them. Of course,
if this switching of running programs from one account to another were
made automatic, then there would be no point in switching accounts
when working on different projects.

The security situation is further aggravated by the fact that software
developers have a "trusted status" amongst the computer-using
community, on account of their specialist skills. Because of this
perception, there is a greater tendency to actually trust the words
and deeds of software developers. Thus the general public are on the
whole far less likely to question the actions, intentional or
unintentional, of software developers. This tendency is inversely
proportional to the perceived status of the software developer, which
is in turn proportional to the extent to which the results of their
work are distributed. So this is contrary (doubly so) to the healthier
purely rational attitude, which would be to treat the actions of _all_
software developers with the utmost suspicion, and the better known
they are, the more so! Since the products of software developers are
frequently duplicated en masse and then widely distributed, the
developers own vulnerability is yet further exaggerated when it
extends transitively to the consumers of their software.

Problem:

Clearly then, the fewer software developers there are, the better, and
also, the the less those few developers do, the better. But many
people seem to enjoy developing software. Should they be deprived of
that right?

The first question is whether it is really software development itself
that they find enjoyable, and not just some particular aspects of it
which are not so much evident in any other activity? The fact that
software developers often have other interests in common indicates
that this is probably not so.

The second question is related to the first. We must ask why they
enjoy software development. If software development were practised
differently, would they still enjoy it? For example, if software
developers had to pay constant attention to issues of security, in
order to ameliorate the vulnerability we have identified, would they
find it equally enjoyable? Every indication is that most would
not. Software projects which have high-security criteria are not as
popular with developers as others which are typically more relaxed,
and where developers perceive they have far greater freedom, and
therefore many more opportunities to be creative. This accords with
our tentative answer to the first question, because the interests that
software developers have most in common seem to do with creative use
of imagination in areas where people can exercise intelligence.

So if we could only find a way to re-employ all the people who enjoy
"coding," in an area where they have far more freedom and opportunity
to express creative intelligence, then everyone will be better off,
except those people who rely on the products of software developers,
because they need software in order to be able to express their creative intelligence! Therefore we need at the same time to find a
way to produce software without using human "coders".

Solution:

It is widely held that "human coders" are absolutely necessary,
because machines simply aren't intelligent enough to write
programs. This is probably true: machines cannot be programmed to be
creative, because creativity is, almost by definition, NOT
mechanical. But this is an error, and that it is so is clear as soon
as one recalls that the difficulty we identified, that people have
with producing secure software, is that there are fewer opportunities to creatively express intelligence: production of secure
software requires a formal discipline, and the results must be in some
sense more reproducible and predictable than those of imaginative and
creative expression of intelligence would be. Therefore it is very
likely that machines could in fact be used to carry out predictable,
disciplined coding, controlled by formal rules which could be shown to
result, when followed very strictly, in the production of secure,
reliable software.

Some may object that this is all very well for communications
protocols and device drivers, but how could software produced by
rigidly following formal rules be used to express, say, artistic
creativity? For example, what sort of a computer game could be
produced by a program following formal rules? What sort of music could
be produced by a computer following formal rules which determined the
notes that were played? This is again an error, one of confusing the
medium with the message: just because the rules are rigid, doesn't
mean the results are not creative expression. One need only listen to
the music of J.S.Bach, or read a Shakespeare sonnet to see this.

Of course the same applies to the process of generating
programs. Software written by a formal process following carefully
constructed rules, as well as being more correct, is in fact far more
beautiful than that constructed ad hoc. This is because there is far
more opportunity to change the expression of a formally specified
process: one simply changes the specification of the generating
process itself, and then re-generates the program. And because the
process is controlled by a computation, the result is typically far
more elaborate than any human mind could conceive.

The evidence for this is in the quite spectacular results which have
been achieved using mechanical processes to generate Fast Fourier
Transform implementations. The process used by the FFTW program's
elaboration of formal specifications has produced several elegant
optimizations of the basic algorithm for special cases, which cases
had not hitherto been published in the technical literature. The same
process also produced some of the published algorithms, which until
then had very probably been considered to be the results of an
essential intelligence. But the intelligence is not in the formal
system, it is being expressed through the use of the system, not by the system itself. This is probably not very different to the
intelligent Human Being's use of the formal system of mathematics to
express intelligent thought. In highly specialised mathematical
fields, people use well-understood methods to derive results. For
example, in [1] which is available from:

   https://www.cs.utexas.edu/users/EWD/transcriptions/EWD13xx/EWD1303.html,

Edsger Dijkstra mentions a method of deriving concurrent algorithms
with correctness proofs. It is disarmingly simple:

    "And then something profound and lovely happened. By analyzing by
    what structure of argument the proof obligations could be met, the
    numerical mathematician Th.J. Dekker designed, within a few hours,
    the above solution, together with its correctness argument, and
    this settled the contest. [...] the pair "c1,c2" implements the
    mutual exclusion, while "turn" has been introduced to resolve the
    tie when the two processes simultaneously try to enter their
    critical sections."

Similarly, a mathematician working on an optimization for a special
case of the FFT algorithm, might use a combination of analysis and
synthesis as a more or less formal process by which she can derive
certain classes of solution, perhaps also with correctness proofs.

There are in fact numerous examples of this in the computing
literature, although it is seldom if ever stated that this is a
recognised technique that is being used. A very obvious example is the
Hindley-Milner type inference algorithm as described by Damas and
Milner in [2]. Here the soundness and completeness are described in
terms of a set of formal rules of deduction, and the structure of the
algorithm W, which infers the type of a given expressions, very closely
follows the available rules in the inference systems for type
judgements and semantic truth.

Another good example is John Harrison's elegant treatment of exact
real arithmetic in [3]. Here a series of proofs of the required
properties of the arithmetic operations on real numbers expressed to
any given precision are used to produce the algorithms which are
written as ML functions to compute those values. The system resulting
from this specification is therefore automatically, because _by
definition,_ formally correct. I am sure numerous other examples could
be found. Often all that is necessary is a subtle shift of one's point
of view, to see the process of deriving the algorithm as a proof
process, or vice-versa, depending on the point of view from which the
author writes the description. Whatever that is, one gets the unifying
process by adding the opposite, unstated aspect: the proof or the
algorithm.

Changing the process of generation of a program is impossible to do
when it is written ad-hoc, unless it is so uniform and regular that it
could in fact have been produced by a formal mechanical process,
because then one can simply treat that program as a formal
specification. But unless it has a highly uniform, regular pattern,
which is not so elaborate that its abstract form is imperceptible to a
human being (*), an ad-hoc program cannot be restructured
automatically. Ask anyone who has applied a large number of patches,
from different sources, to an operating system kernel, say, and they
will tell you this is indeed so. And to see the truth of the clause
(*), try to abstract the FFTW generating algorithm form from a visual
inspection of the code it produces in different cases.

One should not think of this process of proving correctness as a
highly abstract one. It is no more or less abstract than the algorithm
itself, because in this view, the two things, the proof and the
algorithm, ARE THE SAME THING, seen from two different points of
view. This is a common experience, because people only feel they
actually understand an algorithm when the can SEE IMMEDIATELY WHY IT
REALLY DOES WORK. This is why NOBODY really understands public-key
cryptography algorithms: because no-one actually knows WHY they are
secure. Their security, such as it is, rests not on knowledge, but
solely on the ABSENCE of knowledge that they are NOT secure. So they
provide only a certificate, not actual knowledge. That's what ALL
certificates are for: they are used ONLY when actual knowledge is not
strictly necessary, because it is expected to be available at some
subsequent stage of a process. The certificate is therefore used
solely for the purpose of increasing efficiency in cases where it is
more likely than not that, when it becomes available, the actual
knowledge will concur with the certificate representing it.

There is a quite well-known problem on which the reader may enjoy
trying out this technique. One is set the task of determining which of
a certain number of otherwise indistinguishable objects (coins or
footballers, in the two instances we have heard) is either lighter or
heavier than the all others, which are the same weight, and whether
that object actually is lighter or heavier. The difficulty is that the
only measuring device one has available is a balance with fixed-length
arms, and in each version of the problem there is a certain maximum
number of weighings that one is allowed. The task is to describe an
_infallible method_ of determining the _correct_ answer. In some cases
it is obvious, and in others it is clearly impossible. For example, if
one is allowed three weighings to distinguish between one of 64
possibilities. Then the absolute maximum possible outcomes of three
weighings are 3*3*3=9 in number, so one cannot hope to distinguish the
one correct answer from 64 equally probable ones.

In some of these problems the solution is not immediately obvious, and
so it seems unlikely that it is possible, but not because of any
absolute bound on the information that the result of the given number
of measurements could contain. Of course these are the more
interesting cases, and one can use the algorithmic method of analysis
and synthesis Dijkstra mentions to solve them, or indeed to determine
that there is no possible solution. One needs only to consider how one
would convince _someone else_ that the result the method determines in
every possible case is correct; and then analyse the forms of those
arguments, and this will _automatically_ yield the algorithm, together
with its correctness proof. Of course, when the number of available
measurements is critical, as it is in the interesting cases, it is
important to make only those measurements which TOGETHER yield the
most information overall. So "maximizing the entropy," as it were
(choosing those measurements which discriminate most between the
possible outcomes of the WHOLE series of measurements) is the guiding
principle which determines the algorithm that this method generates.

The process as we have just described it is typical of the way
inference problems are tackled in Artifical Intelligence applications
such as are beautifully described by E.T Jaynes in his book
"Probability".

So we hope that we have allayed any fears the reader may have had that
the process of deriving correctness proofs is highly abstract, and
involves a great deal of incomprehensible logical and/or mathematical
symbols, and persuaded her instead that it is really an intuitive
process, and in a strong sense, one that is IDENTICAL with the actual
understanding of the algorithm with which it deals.

We can now go on to consider what Dijkstra's method has to do with
coding secure software. The problem with all security, is what one
might call "the leaking abstraction." This is always a result of some
fixed concrete representation of data as being encoded by
_information_ of some kind. And the leaking abstraction occurs when
that encoding is redundant, so that there are many different possible
encodings of the same data. Simple examples are:

(1) a forged bank-note, where there are two or more representations of
the same one note. Each note carries a unique identifying number,
which is its certificate of authenticity, and the difficulty of
manufacturing a convincing replica means that the certificate is
useful, because it is more likely than not that 'at the end of the
day' the real note will be matched with the actual object of value it
represents. Some fraction of some particular gold bar, for example.

(2) a person in disguise, masquerading as another person who has some
unique privilege; for example, the right of entry to some secure
facility, such as a military compound. Here there is redundancy
introduced into the representation of the individuals, so that, as in
the case of the forged bank-note, the successful infiltrator
compromises the ability of the experimental method to infallibly
discriminate between those who have this privilege and others who do
not.

(3) 'Picking' the five-lever lock on a door. Here the redundancy is in
the representation of the 'certificate' which signifies authenticity
of the tool used to open the door. It is because the lock-picker's
tools are another representation of the genuine key, and the method
the levers implement is not sufficient to discriminate between the
possible outcomes of genuine and false 'certificates.' Of course the
same principle applies to an illicit copy of the key.

(4) 'Tempest' decoding of the electromagnetic emissions from an LCD
connector on a flat-panel computer display. This is possible because
of the repeated scanning of similar images successively displayed on
the screen. This causes multiple, repeated transmissions of similar
signals which allow an 'attacker' to deconvolve the signal and recover
the original modulating pattern, which is the image being displayed on
the screen. If the computer only transmitted the changes to individual
pixels when they changed, this deconvolution would not be possible in
general.

Hopefully the reader will easily be able to produce many, many more
examples of what are all essentially different forms of the same
fundamental phenomenon. Abstractions which are realized in fixed
concrete representations invariably leak, simply because they
introduce redundancy into the representation of what are supposed (or
assumed) to be unique events. So if we could only find a method of
making abstractions in such a way that their concrete representations
were always changing, then we would have solved the problem of
computer and communications security in general, because there would
be no fixed 'certificate of identity' for the 'attacker' to forge. And
dually, there would be no redundancy for the 'attacker' to 'key into'
in the information which represents the data that system processes.

In [4], Dijkstra presents a method of designing 'operating systems' in
which layers of abstraction are successively introduced, one on top of
the other, and in which some concrete representation of the physical
hardware of the machine 'disappears' as each new abstraction is
added. The disappearing physical objects are replaced by multiple
virtual representations of objects with the same or similar
functionality. I.e., forgeries of the real identifiable hardware. The
paper does not give detailed examples of how this is done, but it
seems to us more than likely that using Dijkstra's other idea of
designing algorithms by a process of analysing what would be required
of a proof of correctness, and taking the view of this analysis as
being guided by a principle of maximizing the information content
(i.e. minimising the redundancy) of successive measurements, one could
formulate a method for deriving a general class of system designs of
the kind Dijkstra describes. One would start by considering what it is
one would need to do to convince someone else that a system is secure
(i.e. that the data are represented concretely with minimal
redundancy, or equivalently, maximum entropy.) For example, that the
data stored in a disk or core memory was 'mixed up' as much as
possible. This is achieved in Dijkstra's example system by
virtualising the physical pages and storing addresses as 'segments'
which are mapped by a virtual process onto physical pages of
memory. So it is only via the virtual page-mapping process that the
segment identifiers are meaningful. But the virtual page-mapping
process is not visible to any other process except via the highly
restrictive synchronisation primitives via which processes are
constrained to communicate.

In [1] Dijkstra mentions:

  "In the beginning I knew that programming posed a much greater
   intellectual challenge that generally understood of acknowledged,
   but my vision of the more detailed structure of that vision was
   still vague. Halfway [through] the multiprogramming project in
   Eindhoven I realized that we would have been in grave difficulties
   had we not seen in time the possibility of definitely unintended
   deadlocks. From that experience we concluded that a successful
   systems designer should recognize as early as possible situations
   in which some theory was needed. In our case we needed enough
   theory about deadlocks and their prevention to develop what became
   known as "the banker's algorithm", without which the
   multiprogramming system would only have been possible in a very
   crude form. By the end of the period I knew that the design of
   sophisticated digital systems was the perfect field of activity for
   the Mathematical Engineer."

[1] Edsger W. Dijkstra. EWD1303

    https://www.cs.utexas.edu/users/EWD/transcriptions/EWD13xx/EWD1303.html

[2] Luis Damas and Robin Milner,
    Principal Type-schemes for Functional Programs,
    In: Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages  ACM, 1982, 202--212.

    http://prooftoys.org/ian-grant/hm/milner-damas.pdf

[3] John Harrison, Introduction to Functional Programming.

    http://www.cl.cam.ac.uk/teaching/Lectures/funprog-jrh-1996/all.pdf

[4] Edsger W. Dijkstra "The Structure of 'THE'--Multiprogramming System"
    Commun. ACM 11 (1968), 5:341–346.

    http://www.cs.utexas.edu/users/EWD/ewd01xx/EWD196.PDF

Beware the Good and the Wise

This is a reply to:

    http://lists.gnu.org/archive/html/guile-devel/2014-09/msg00118.html

> 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).

No I wouldn't have guessed that, because I cannot understand it at
all. For example, it is possible to formalise classical logic, and
also intuitionistic logic. Similarly, one can formalise Euclidean
geometry and also numerous non-Euclidean geometries, and one can
formalise higher-order logic and also first-order logic. So what does
the possibility of formalising a system tell you about whether or not
it is 'universal'? All I can see that it tells you is that that system
is not necessarily inconsistent, which in itself is hardly saying
anything at all.

> 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).

This elevator would wait until there were balanced loads, so that the
weight of those wishing to descend would lift that of those who wish
to ascend, and very little energy would be required to run the system?
I was thinking about this a few months ago. Here in Bolivia we have a
3km potential difference in height between La Paz and the
Amazon basin. The mass of people and goods descending might be very
similar to that of those ascending. So I was wondering if it would be
feasible to build a funicular of some kind.

Whether this would be perceived as unfair or not is entirely a matter
of education. If people were educated properly they would know that it
is unjust to profit from anything which wastes resources and degrades
the quality of life of other people. There is nothing particularly
difficult about this idea. But people who lack education often justify
their moral lassitude by claiming all moral values are relative. "It
all depends on your education!" they say. And they're right: it
depends on whether or not you were educated. So the only reason that
universal ethics "don't exist" is that a substantial proportion of
people are for all practical purposes uneducated.

> 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).

I don't understand this at all, but then I have never understood
anything I read of Kant. And the only thing that I read and understood
which anyone else wrote about Kant's writing was, I think, by Roger
Scrouton, (but it was a long time ago, so I could be wrong) in a
little book called "Kant," to the effect that "Kant's thought is
incomprehensible."

> 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.

I don't recall reading anything like "it is good to give what is due"
in Aristotle. The word 'due', in English, carries a sense of
ownership, obligation or debt, and neither of the books Aristotle
wrote on ethics have any of that sense about them: they are all about
fortune, God, judgement and knowledge. Are you sure you are not getting
Aristotle mixed up with Jesus Christ when he said, concerning the
payment of taxes, "Give unto Caesar that which belongs to Caesar"?

If I had to summarise Aristotle's many hundreds of pages on ethics in
a few words I would say that, since the essence of a thing is that
thing's special nature, which is also the reason or purpose for which
that thing exists; and since the special nature of man is our capacity
for rational thought, that is also the reason or end to which we
exist. So what is good for man (i.e. all people, so universal) is the
exercising of 'his' capacity for reason.  Therefore whenever people
reason to the utmost of their ability, they are being good. That is,
excellence in thought is right or moral, and anything less than this
is wrong or immoral.  It follows then that all evil we can know is
simply human error, or stupidity, and nothing more. And the greater
good is God, who is life itself, and the living self dependent
actuality of thought, which is eternal and most good; so the reason or
purpose (the final cause, in the teleological language) of human life
is to realize, here on Earth, the eternal living mind of God. And we
do this through reason, and only through reason.

Rather than reading commentaries on Aristotle, I recommend going
straight to his own writing, which I have always found to be far, far
more easily understandable than any commentaries. These always seem to
be more concerned with comparing and classifying his "thought," but
without actually thinking any of it.

----

> 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.

The conflict you see is not unfortunate or "unhelpful"; quite the
opposite: it is the war against evil. You will see this wherever
idiots talk rubbish without thinking about what they're saying. It
isn't actually conflict, because the idiots typically can't respond
with anything except a series of ever more convincing demonstrations
of their complete and utter stupidity. It seems to be some kind of
public self-humiliation rite they need to go through. It's best just
to observe, and try not to laugh at anyone.

> I would suggest the following proposition to Ian Grant, I think it
> may be helpful:

I don't think you thought at all, I think you just do what millions of
people do, and that is you don't actually think, you simply write and
say what people expect one to write and say in such and such a
situation. Most people "think" that's what thought actually is.

> 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.

What do you mean by 'actual observed phenomena'? If you know anything
at all about molecular biology then you know that polypeptide
synthesis is not something that is actually observed, it is an
abstract process which exists purely as a series of inferences from
quantified experimental results. So it is a mathematical model. What,
then, are the "interesting inferences" to which you refer? And why are
they interesting? And why is it "worthless for making predictions
about how actual ribosomes synthesize polypeptides"? As you can
probably tell, I don't have the faintest idea what you are trying to
say, but I very much doubt that you do either!

> Quite similarly, the hypothesis suggested by Milner, I think it was
> "properly typed programs can't be buggy" appears not to hold
> water.

The only similarity I see is that of nonsense with nonsense. You can
be quite sure Robin Milner did not ever write or say anything like
this. Standard ML has been used all over the world, for over 20 years
now, to teach students programming. So no-one in their right mind
would claim that typed programs can't be buggy: that's an utterly
ridiculous idea. The 'hypothesis' you refer to, is the actual
knowledge that type checking in fact catches many common
programming errors. And I have never heard anyone who has actually
used a typed programming language try to refute this! Even C
programmers know it.

> It is a good, consistent, even solid theory,

It "appears not to hold water," but it's nevertheless "good,
consistent and solid"? Bullshit! It's none of these, it is a
completely fucking stupid theory!

> but it doesn't capture the nature of programming. And it doesn't
> deliver on the promise.

No it can't, because the "promise" is something idiotic which you just
invented in order to have something to say for yourself which you
thought might suit your image as the wise-old-man of scheme-land. As
far as "the nature of programming" goes, if you mean by this "the
common practice of programming," then I think the only thing that
could capture that nature would itself be complete and utter
nonsense. So your "good, consistent, solid theory that doesn't hold
water" actually does do that, in buckets! But I am not interested in
"capturing the nature of programming," I am only interested in
changing it, because it is stupid and evil.

> 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.

You don't need to tell me that. See the following, which I wrote
several months ago, which is all about the stupid mistakes I made, and
bugs in my Standard ML implementation of, guess what? The
Hindley-Milner type checking algorithm!

   http://livelogic.blogspot.com/2014/07/hindley-milner-type-inference.html

> I just wanted to say that maybe your conclusions have been premature
> and lacking the statistical evidence (lack of evidence isn't
> itself a proof of the contrary).

No Oleg, your summary of "my conclusions" is premature. You have just
spouted off a load of utter drivel, because you did not take the
trouble to properly read anything that I wrote before telling me that
it is wrong. See the PDF referred to in the 'original post' as far as
these lists are concerned, which is here:

   http://lists.gnu.org/archive/html/guile-devel/2014-08/msg00064.html

I don't have any advice for you, but Ed. does. This is from:

    http://www.cs.utexas.edu/users/EWD/ewd01xx/EWD196.PDF

      "Be aware of the fact that experience does by no means
    automatically lead to wisdom and understanding, in other words:
    make a conscious effort to learn from your precious experiences."

Ian