On Sun, Jan 11, 2009 at 12:52 PM, Geoffrey Irving <[email protected]> wrote:
> As far as I can see, the only way to satisfy both of these is to have
> a well-defined strict mode, and require any compiler that goes outside
> strict mode to produce extra annotations that reduce the program to
> strict mode. I.e., compilers can use any proof generation technique
> they like, but the proof must be in the form of a new strict-mode
> program with obviously identical semantics.
> [observations on sociological difficulties of checking in an sharing the
> weaker portable language]
Hi Geoffrey,
Sorry, I only now read your response after sending my own. I think
we're saying about the same thing. The only salient difference I see
is that by reducing the weak language to include only a really dumb
(and easy to specify) proof checker, my weak language would not be
human readable or maintainable. One would have no practical choice but
to program in the strong language but checkin and ship the weak
language. Whether this is a comparative strength or weakness, I don't
know.
--
Text by me above is hereby placed in the public domain
Cheers,
--MarkM
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
