Yes, the primary reason being the bootstrapping problem. But because Dafny can already can generate C# code, that should not be a major problem. It also allows for a gradual conversion where more and more parts are generated from Dagny sources.

I know that maintaining a compiler in its own language poses some problems when you want to extend that language with additional features.

Because compilers are rather complex problems, they can be viewed as a testing stone for a language.

I think it would be nice to have a formally verified compiler. That is a bit more than proving that the sources are correct. But because formally verified compilers are rare, it could promote the usages of Dayne.

I am aware that it would be quite an effort to make it self-hosted and even more to formally verify it correctness.