[clark800]

I'm working on an open source pure functional programming language called Lambda Zero that aims to be a simple and elegant base language from which to derive more advanced languages and eventually a foundation of mathematics. Like Haskell, it is basically just the lambda calculus with a bunch of syntactic sugars, so it's more a process of discovering the foundations of computation than inventing an arbitrary new language.

There is currently a bootstrap interpreter written in C that is under 2000 lines of code, a self-interpreter (~1200 lines), and a static type inferencer written in Lambda Zero (~400 lines). I'm currently implementing pattern matching lambdas and algebraic data types and I have a long roadmap of things to do. It would be great if someone was interested in writing an optimizing compiler for Lambda Zero in Lambda Zero.

https://github.com/clark800/lambda-zero

[anonlastname]

> and eventually a foundation of mathematics.

So it will have a proof capability like Coq?

Is there any new theory behind this system? What is your vision in this regard?