IPL: Intuitionistic Programming Language (2013)

IPL: zero abstraction penalty

The intuitionistic programming language (IPL) is an open source programming language, combining a very high level of abstraction with compilation to efficient LLVM bytecode.

Only a small fraction of the constant increase in computer capacity is turned into direct benefits for users. Large programs require a higher level of abstraction and more bookkeeping to remain modular, malleable, and maintainable. Indeed, large scale program development would be nearly impossible without innovations like type systems, automatic memory management, function objects, and separation of concerns provided by modules and classes.

Still, conventional wisdom dictates that abstraction comes at a cost: not so with IPL, where first class functions, procedures, and objects are all compiled to efficient LLVM bytecode with zero abstraction cost.

The semantics of IPL is based on intuitionistic type theory extended with a component model it compiles to LLVM bytecode using a novel algorithm based on term rewriting. The IPL compiler is very small: less than 10,000 lines of OCaml code.

IPL provides

• zero abstraction penalty,
• a very high level of abstraction,
• excellent run time performance,
• strong static safety guarantees,
• predictable performance without GC pauses,
• support for verification and testing, and
• a composable effect system based on free monads.

The combination of these features is made possible by an algorithm that eliminates high level constructs at compile time. The limitation implied by this algorithm is that mutable complex state has to be region based (global or local).

IPL is currently in the early stages of development and there are many opportunities to make a large impact on its future direction and for further innovation in the space.

If you would like to know more, ask a question at the discussion group.

On the specific topic of making verifiable functional programs: if you like to write code to verify, then you may want to have functional-like languages that aren't so heavy in terms of runtime requirements. Like, if you are trying to verify aerospace software, or something, then, maybe, you don't want a garbage collector. That will make whatever verification work you're doing much more relevant to the industry, instead of sitting too far up the stack, as languages like Scala and F# probably do. Don Syme. “Panel: The future of functional programming languages”.
Robin Milner Symposium, 15-18th April, 2012.

I do not think that the search for logically ever more satisfactory high level programming languages can stop short of anything but a language in which (constructive) mathematics can be adequately expressed. Per Martin-Löf. “Constructive mathematics and computer programming”.
In: Logic, Methodology and Philosophy of Science, 1982.

from Hacker News https://ift.tt/4drFmJH