On Thu, Feb 26, 2009 at 5:47 PM, <[email protected]> wrote: >>On Thu, Feb 26, 2009 at 12:47 PM, Rick R <[email protected]> wrote: >>I'm having trouble understanding this proposal. BitC doesn't need to >>define a single integral type. We support multiple sizes of machine >>integers directly. >> > > Why? My (minimal) familiarity with proving stuff is that you've got > enough of a problem with bounded integers, which may overflow (which > is a runtime error and you want to avoid these, natch). But instead of > one type of bounded integer you have several...
Because BitC is focused on systems programming, and we therefore need to deal concretely with things like hardware registers, cache line sizes, and things of that sort. Matters of data layout in systems programs are prescriptive. The formal inconveniences that you identify are real, but they cannot be solved at the cost of failing to satisfy pragmatics requirements. This is why ML and Haskell will not ultimately succeed in this sort of space. In this domain we need to be able to write applications that are provably allocation-free and provably bounded space. In the absence of bounded integers that is not possible. We also want to be within 1% to 1.5% of the performance of aggressively hand-optimized C (and privately I'ld like to *beat* that performance). That definitely cannot be done if we build any significant overhead in at the level of integer arithmetic. BitC does provide an unbounded integer arithmetic capability, and for many applications that is the right thing to use. It isn't good enough to write operating systems. > So, why bound integers at all? It should be possible to simply declare > that x is an int (meaning unbounded signed) or a domain-convenient > subset like -12..45 (like pascal) and map appropriately to the > underlying machine... Range constraints incur a discharge obligation. In the general case, this is an unsolved problem in the literature. > Actually, maybe another front. IIRC the original dec alphas were > restricted to 32 & 64 bit integers... Yes. And this is one of the reasons that the alpha failed. It was *horrible* at handling character data, for example. shap _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
