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