On 12 Feb 2015 16:02, "Jonathan S. Shapiro" <[email protected]> wrote: > > 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.
I disagree, and because my own project depends on this, I would be interested to understand your reasons for thinking this. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
