Thread Links Date Links
Thread Prev Thread Next Thread Index Date Prev Date Next Date Index

Re: Motion P1788/0024.01: Rounding Mode as Operation -- discussion period begins



Baker, George, Ulrich and all P1788

On 18 Apr 2011, at 11:33, Ralph Baker Kearfott wrote:
> Was required processing missed on the 2010-10-05 item?  Was it formally
> put forward as a motion?  Are you referring to
> "Discussion paper: what are the level 2 datums?"

As I recall, that discussion paper never made it to a formal motion, because I was rapidly convinced by Nate and Arnold that I had the wrong end of the stick, which led to my current level 1 v03.1 document with the unified algebra of decorated intervals, bare intervals and bare decorations.

So I think Ulrich's should be motion 24.

Yes, I am somewhat worried about our timetable. Having done the bulk of my Cardiff teaching this spring, I will now get on with revising v03.1 in light of comments, mainly by Arnold Neumaier. I wish I had more nitty-gritty comments from other people. But let's see how I get on in next few weeks. 

I am encouraged to hear that Ned Nedialkov and his student Bingzhou are looking at my v03.1 from the viewpoint of *formal verification*. NOT verifying my proofs; BUT they will assume the correctness of the decoration model and look at what is involved in writing formally verifiable algorithms on top of it. 

This is a significant development. If it goes well it will show we have a standard that can actually be USED to promote the ideal of "Reliable Computing".

Probably Juergen's proposed motion about constructors can go ahead essentially orthogonally to my v03.1 stuff. I look forward to that.

John