Would this language be useful for implementing compilers and formally proving things about them?
yes thats the main reason, agda , coq similar ideas