[cap-talk] controversial article

[Mark Miller]

On Thu, Jul 2, 2009 at 12:17 PM, David Wagner <daw at cs.berkeley.edu> wrote:

> Matej Kosik  wrote:
> >I hope that it is correct to say that all object-capability programming
> >languages can be used for creating software systems that are defensively
> >consistent but none of these languages (or platforms) can be used for
> >creating defensively correct software systems. (?)
>
> To be pedantic, they can plausibly be used to build defensively
> correct software systems (they're Turing-complete, after all); it's
> more that those languages don't provide special support for reasoning
> about or ensuring defensive correctness.  So those languages don't
> provide any extra help; if you want defensive correctness, you're
> on your own.


To be meta-hyper-turbo-pedantic, I claim this is false. A program is correct
only if it relies only on specified properties of its platform, and not on
unspecified properties of its platform's implementation. The specified
semantics of all these languages either
1) assumes away the possibility of memory exhaustion, in which case their
specification is not implementable (or only implementable up to fail-stop,
which is inadequate for progress guarantees), or
2) they allow an out of memory condition to occur any step of computation
that may allocate memory, including function/method calls in languages that
allow recursion.

In either case, even a program as simple as

    function main() { foo(); }
    function foo() { print("hello world"); }

as expressed in almost any language in use today cannot be said to correctly
implement the spec "prints 'hello world'." The most that can be said is that
it will either do so or it will run out of memory. In Fortran 4, Occam, or
any of the bare handful of languages without recursion or implicit dynamic
allocation, given an appropriate and realizable spec, we can at least say
that the above program will either fail to load or correctly run to
completion. In these languages, one can write programs that would be
defensively correct *given* that they successfully load. This is another
useful approximation of defensive correctness -- perhaps the closest
practical one.

-- 
Text by me above is hereby placed in the public domain

   Cheers,
   --MarkM
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.eros-os.org/pipermail/cap-talk/attachments/20090702/3de6b788/attachment.html