[Haskell-cafe] Re: Maybe and partial functions

[oleg at pobox.com]

Neil Mitchell wrote:
> newtype N1 = N1 Int
> (put that in a module and don't export N1)
>
> define the constant 2, define the increment operator, change div and mod.

That is precisely what I would have done.

> Now we've mainly got a proof in the type checker, but we still don't
> actually have a proof for our core N1 definition - but I think that is
> probably ok, provided it is a common core which can be reused and is
> minimal.

Any proof of totality of the original digits-of-e code must first
prove or postulate that incrementing a positive number gives the
positive number. So, one must prove/verify/assume the basic properties
one way or another. In the lightweight static capabilities approach,
these basic lemmas/properties/axioms are collected in modules, which
can be verified once and for all and then used in various parts of the
program. Accommodating the security kernel in those parts of the
program does not seem to be a burden. In return, we get assurances of
the simple kernel in those parts of the program without the need to
run the verification algorithm all over again (on the possibly complex
pieces of code). The idea that data type abstraction can enforce
complex invariants was advocated back in 1973 by James H. Morris (the
father of the guy who released the `Morris worm'), in the CACM paper
"Protection in Programming Languages".

	http://www.erights.org/history/morris73.pdf