An approach for implementing TUNES

[Laurent Martelli]

>>>>> "Faré" == Francois-Rene Rideau <fare@tunes.org> writes:


  >>> Proving the correctness of drawing routines requires a model of
  >>> the video (beware that things are often not exactly the same
  >>> when done by the video hardware, and that discrepancies should
  >>> "leak" into a security breach when misspecifying what happens
  >>> with video or other inexact I/O).
  >>  That is true... If we specify that operation FOO only puts a
  >> pixel on the screen, when it actually makes the monitor blow up,
  >> then anyone who the security privilege to put a pixel on the
  >> screen will be able to perform operation FOO and thus make the
  >> monitor blow up.
  >> 
  Faré> The problem is much more subtle: if you formally define
  Faré> "drawing a line" by a given routine, but the actual hardware
  Faré> or library routine will draw the line in a different way
  Faré> (displacing a few pixels, doing anti-aliasing in a different
  Faré> way, etc), then there will be a discrepancy between your
  Faré> assumptions and the reality, and an ill-intentionned user or a
  Faré> ill-driven program might use this discrepancy to prove an
  Faré> absurdity in your system, whence to be able to have the system
  Faré> admit any inconsistent axiom.

  Faré> Specifying operations as conceptually "simple" as "drawing a
  Faré> line" in a way that be both correct and useful is _quite_
  Faré> challenging!  The same could be said of "real number"
  Faré> arithmetics, all the more when you want to relate your "real"
  Faré> arithmetics implementation (IEEE or not) to approximations of
  Faré> actual mathematical numbers.  Again, this does NOT mean that
  Faré> the task is unfeasible: when people design programs so as to
  Faré> be correct, they do, in their right mind, do this work of
  Faré> relating implementations to specifications, so that, when
  Faré> programs are actually correct, there _is_ a way that could be
  Faré> found to prove it.  But this is nonetheless a very complex
  Faré> task for which tools are currently lacking.

I tend to think that there should be several specifications of
"drawing a line". Because, sometimes you just don't care if
antialiasing is done an how it is done, and sometimes you really care
about the precise value of each pixel (if are implementing
antialiasing for instance). Given the context, one level of
abstraction is better than others.

Laurent