Banneker
An extremely work-in-progress language with dependent types.
I am trying out a "functions are vectors" variation on Martin-Löf intensional type theory that is probably ill-considered, inefficient, and nothing here works or is even guaranteed to compile :)