Comment by 3lambda

Would this language be useful for implementing compilers and formally proving things about them?