Manifold. Another experiment in dependently typed languages, this time with some quantitative type theory smooshed in.