Can Motion 8.02 support proofs of correctness?
P1788, Nate, Arnold
Two points:
A.
Studying Motion 8 and its rationale I have long had the feeling that
the wool is being pulled gently over the eyes, and at last I think I
see why. It is because the present decorated interval scheme does not
enforce -- and unless its semantics is made more precise and
restrictive it is actually incompatible with -- something that I
regard as crucial to the long term success of an interval standard.
Let me try to explain.
1. [Uncontroversial] I believe that it should be possible to write
interval algorithms whose correctness is provable, not just when
everything goes OK, but also when exceptions occur.
I am not thinking of formal proofs, but of proofs written at the
normal standard of mathematical rigour, such that they can be peer-
reviewed.
2. [Probably uncontroversial] I believe that the proper setting for
such algorithms is Level 2. That is:
- There is a finite set of level 2 objects, and operations on them,
that provides all needed facilities both for writing interval
algorithms with possible exceptions, and for proving the
correctness of such algorithms.
- In the motion 8 scheme these objects would be bare intervals
(say, for simplicity, of IEEE binary64 format), bare decorations,
and decorated intervals of the same format.
In a flagspace scheme there would be a different set of objects.
- There is no need to descend to level 3-4 implementation details
to express proofs, indeed a "proof" that does so is invalid.
3. [Possibly controversial and I am not a good enough computer
scientist to know how to express this well]
The semantics of programs at Level 2 must be such that the
value of an object cannot be changed "by the side door". Possibly
this is the same as requiring objects to be "immutable" in the
Java sense -- e.g. see
http://www.javaranch.com/journal/2003/04/immutable.htm
which gives this rough definition:
* Mutable Objects: When you have a reference to an instance
of an object, the contents of that instance can be altered.
* Immutable Objects: When you have a reference to an instance
of an object, the contents of that instance cannot be altered.
In particular, the decoration of an interval is to be fixed when it
is created, and cannot be changed by subsequent history. (This does
not preclude doing things like xx = yy/xx, which makes xx reference
a brand-new value that may have different decoration from xx's old
value.)
My reason for honouring item 3 is: code that violates it is the very
devil to prove correct, and its behaviour in a multithreaded context
may be indeterminate.
HOWEVER...
The sample code that Nate offered, to show how Decorations can
implement Global Flags, works (I think) PRECISELY because it violates
item 3. Namely, if xx is a decorated interval, its "decoration" field
xx.dec is actually a pointer to the global flag F. An operation on a
different interval yy can change F; then, on inspecting xx you find
that xx.dec has apparently changed, without you doing anything to xx.
HENCE
The decoration scheme that Nate and Arnold have produced is a useful
_mechanism_. Motion 8 intentionally defers various semantic issues,
in keeping with the "mechanism" emphasis.
But the above shows that without further semantic rules, the scheme
is _logically incompatible_ with item 3.
Rather than offer his sample code as the solution to a problem, Nate
should have made it a dreadful warning of what should NOT be done.
(Maybe privately he thinks that, anyway.)
My conclusion is that I cannot support Motion 8 as it stands, and I
will think how the semantics need to be more closely defined.
B.
Motion 8 §1.2 says that a decoration trit "characterizes part of the
history of a computation", which is fine by me. Every boolean
attribute of a segment of computation history, that I can think of,
can be regarded as an event. So a trit is supposed to say "between
points A and B of the history, event E did happen (+); or didn't
happen (-); or I'm not sure if it happened or not (0)".
But of the candidate trits in 3.4:
Valid
Defined
Continuous
Tight
Bounded
Standard
Empty
Entire
only the first four are attributes of a segment of computation
history. Surely the others are attributes of the individual interval?
Or is "Bounded" about the event "all the intervals produced (or
used?) within the given segment were bounded"? -- that doesn't seem
very useful. So there is some confusion here, which the authors may
be acknowledging in the first paragraph on page 6.
Regards
John Pryce