On Wed, Jan 7, 2015 at 8:23 PM, Jonathan S. Shapiro <[email protected]> wrote: > On Wed, Jan 7, 2015 at 5:32 PM, Geoffrey Irving <[email protected]> wrote: >> >> You're right that not *all* field offsets can be known at compile time >> if we treat modules as large structs, but that's essentially identical >> to symbol offsets not being known until runtime link time. It might >> require treating "structs that are modules" slightly specially in >> terms of who is enforced to be known at compile time when, but it >> doesn't seem technically difficult. An "object file" just becomes a >> special variety of big struct. > > So there's an interesting mid-point here. It may be possible to design a > type system for separate compilation in which the run-time requirement is > relocation rather than inlining. I'm skeptical, but if that is possible it > presents a qualitatively new design point.
Excellent. I feel like this ability is essentially "free" once you have a sufficiently low level language with proofs, but admit that the qualifier is a big one. Geoffrey _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
