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