On Thu, Feb 12, 2015 at 2:06 AM, Keean Schupke <[email protected]> wrote:
> To expand on my last point, I think a pure lambda calculus can model any > computation. I think a type system restricts the admissable lambda terms to > a subset with your desired semantics. I think you can then directly compile > that semantics. > > For example starting from a pure lambda calculus you can have a type > system that admits terms with the same semantics as C... > This is an excellent summary of the "pure type theorist's" view of things. It is correct only because the pure type theory view does not consider computational performance (latency) to be part of semantics. In this view, a program that takes 100,000x as long to run as it should is perfectly acceptable, because it models the computation. The user who dies still waiting for that answer may have a different opinion. > You can then compile this directly to assembly in the same way a C > compiler does. > No. You can't. Because your definition of semantics excludes essential information that the C compiler requires in order to produce the assembly code that it produces. > Maybe this isn't right for BitC, but I think it is worth mentioning. > BitC's purpose is to find an acceptable reconciliation between pure type theory and the pragmatic requirements of systems codes. For systems programs, performance is part of semantics, and we are therefore concerned with concrete issues in addition to abstract issues. The two do not always reconcile gracefully. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
