Surface: a dependently-typed language with a proof refinement–style typechecker This is a learning project/experiment. Don’t expect it to be useful.