Re: Can Motion 8.02 support proofs of correctness?

["Nate Hayes" <nh@xxxxxxxxxxxxxxxxx>]

John Pryce wrote:
> P1788, Nate, Arnold
> 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.)

No, not at all.

That example shows that global flags (or flagspace) are just a form of
decorated intervals. Just like IEEE 754 global flags can be thought of as a
form of "decorated floating-point" numbers.

The abstractions in motion 8 don't violate item 3, since only operations
producing a new interval can change the decoration trits; so with proper
thread syncronization, the behavior in a multithreaded context is entirely
consistent.

Nate