[bitc-dev] Retrospective: The Issues with Type Classes

Geoffrey Irving irving at naml.us
Sun Apr 15 17:09:10 PDT 2012


On Sun, Apr 15, 2012 at 5:00 PM, Jonathan S. Shapiro <shap at eros-os.org> wrote:
> On Sun, Apr 15, 2012 at 4:36 PM, Sandro Magi <naasking at higherlogics.com>
> wrote:
>>
>> A JIT would solve all of Jonathan's problems, except keeping the TCB
>> small and auditable. At the moment, the situation is very much: small
>> TCB, inlining, separate compilation, pick any two.
>
>
> Yes, though JIT has a huge systemic cost when it is applied to all of the
> programs in a system.
>
> I have no objection to using JIT techniques. In fact, I think that doing so
> is a very good idea. What I want to avoid is designing a language whose
> only sensible compilation method relies on JIT. Maintaining the ability to
> do separate compilation is a necessity, in my view.

"Pick any two" seems extremely fundamental, though: the only way I see
to completely get around it involve theorem proving (e.g., a verified
JIT, or fully specified semantics of functions).  That aside, the easy
pragmatic approach is to pick a different set of two on a function by
function basis.  If the language is structured such that basic
arithmetic can be inlined and large functions can be separately
compiled, doesn't that solve the problem?  Is there any other solution
available even in principle?

Geoffrey



More information about the bitc-dev mailing list