Re: [Fresco-devel] [ReFresco 03] Proposed network architecture overview

--- Tobias Hunger <[email protected]> wrote:
> C Y <[email protected]> wrote:
> > http://freedesktop.org/Software/xcb/usenix-zxcb.pdf
> 
> That paper is an interessting read, thanks for pointing it out! I
> have to admit that I am lost with the Z syntax and all, but I think
> I got the drift:-)

No worries - Z syntax isn't my speciality either :-).  I figure it,
like any worthwhile tool, can be learned if the benefits outweigh the
annoyances.

> Unfortunately I can't find any "Learning Z" material on the net, so I
> doubt that we will end up using Z much. 

Well, these might be places to start:

http://www.usingz.com/
http://www.usingz.com/text/

http://spivey.oriel.ox.ac.uk/~mike/zrm/

http://www.zuser.org/zbook/

The EROS guys might also have some suggestions - I think they have
actually formally verified a couple of the features of their system,
although I don't know if they used Z.

> We do use UML with its various diagrams and other state diagrams at 
> times, even if those tend not to get published on the website;-)

Yes, I don't imagine they would help casual users much :-P.  There
might be some UML related Z tools here: 
http://www-lsr.imag.fr/Les.Groupes/pfl/RoZ/
but lord knows if the Fresco project meets their criteria for use of
the software.  And they seem to depend on an evaluation version of one
of IBM's products for free use.  Maybe someone can sweet talk both IBM
and the RoZ guys into being sponsors of Fresco :-P.

> PS: Maybe you got some material on learning Z or maybe you want to
> help improving the design with formal proofs?

The links above appear to be complete online books on Z - sometimes not
having new editions of things printed can be a good thing ;-).  I
myself do not have time enough to become proficient with both Fresco
design questions and Z proof notation, unfortunately - grad school is
rather unforgiving in that regard.  My thinking ran something like
this:

a)  Fresco is an all new, complex, and possibly long term answer to the
problems of computer graphical display.

b)  Security is rapidly becoming the #1 concern in the computer world
(features having been well enough addressed so people can do useful
work) and the combination of EROS and a capabilities based Fresco with
both backed by proof logic would be a POWERFUL force in the computer
world.  Being able to say with confidence that it was done right the
first time is becoming important in a world where people put computers
on the net without updating them. 

c)  Since Fresco's core designs are under discussion (unlike those of
X), Fresco might be in an ideal position to try and combine the tools
of open source, proof tools, and EROS style security thinking to kick
the computer world into not only the next generation of graphics, but
the next generation of security.

d)  However, since talk is cheap and I'm not able (at least for a
decade or two, groan) to carry the ball, I thought I'd put my thoughts
out and see how actual intelligent people react to them ;-)

CY


__________________________________
Do you Yahoo!?
Yahoo! Hotjobs: Enter the "Signing Bonus" Sweepstakes
http://hotjobs.sweepstakes.yahoo.com/signingbonus