On Sun, Jan 11, 2009 at 1:03 PM, Mark Miller <[email protected]> wrote:
> 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.
Glad we're on the same page. :)
I think the strict language would need to be at least as powerful as
bitc-with-no-dependent-types, plus just barely enough dependent type
inference to handle
(if (= b 0) (/ a b) (throw ...))
without any annotations. I.e., much more than bare bones PCC.
Anyone who wishes bitc didn't have dependent types could program
purely in strict with no machine assistance, and call a few library
functions to handle the above idiom. I think this is important from a
sociological perspective, since it's critical that a programmer with a
dumb compiler and no knowledge of dependent types is able to program
without them (with the possible exception of small areas of the code).
If this is a normal occurrence, it would force programmers who do use
smarter tools to embed their annotations, and prevent the strict
language from degenerating into something like assembly (generated by
tools only).
By the way, I'm really thrilled that bitc is undergoing this kind of
discussion! It seems like bitc has a high probability of growing all
the pieces I've been imagining over the past few years when I think
about my perfect language for simulation programming, so I apologize
if I lose control of my excitement and end up off-topic.
Geoffrey
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
