I thought BitC was based on TAL, but I might have got that wrong. In any case, I think TAL is a kind of proof carrying machine code. This is related to what I described about 'C' code because that too is a method of proving things about the code.
I realise that this might not be what BitC is aiming at, but the idea I proposed solves some problems I am interested in, which is parametric polymorphism of C functions and managing the effects (via a monadic effects system) of an imperative language like 'C'. It seems that iterative looping is more readable than maps and folds, so I want the high readability and performance of an imperative language, but with the type system of something more like Haskell (in fact going further than Haskell with a logic language in the type system like a logical framework allowing theories about code to be proved). I think the language I currently envision would be something like the good parts of JavaScript as it will have type inference unlike 'C', with algebraic data types, records as modules and type - classes using implicits. One important rule is no cost should ever be hidden from the programmer, so that an add would be a single machine code instruction, and anything that slows code down (indirection, virtual functions) has to be explicitly specified by the programmer. All values will be unboxed, and as there is no garbage collector, all pointers direct. Memory safety will be achieved by effect tracking (making sure references don't escape containers) and the proof system (proving all allocated blocks get freed on container destruction). I imagine the low level inside containers and low level algorithms will look a lot like C paying attention to exact memory layout and bits and bytes. The higher level will be more functional plumbing things together. The idea is the imperative code fulfils proof obligations that it has well behaved value semantics, and can then be used in 'pure' functional code (without having to be in a monad). The pure functional code is a simple stack based implementation (hence no performance penalty for heap or GC, heap memory would only be available imperatively inside containers). The key benefits to the programmer are support for a generic programming model as in Stepanov's "Elements of Programming" done cleanly through the type-system, and effect control enforcing RAII style use of memory and other resources. You could write a vector container internally imperative and as good performance as C++, and then use it in pure functional (stack based) code, or simple imperative code with value semantics. Keean. On Thu, Feb 12, 2015 at 12:08 PM, Keean Schupke <[email protected]> wrote: > We can write a 'C' emulator in pure lambda calculus, or perhaps better, > compile 'C' to pure lambda calculus as a target. The types of these pure > lambda terms would be the types of the C terms. That's exactly the kind of thing I was saying doesn't solve anything, and just transforms your problems into more verbose ones. And you do realize that that's nothing like what TAL does, right? _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
