Looks interesting. I saw some C# files, from which it seems it is implemented in C#. Is there going to be an implementation in Dafny?
Looks interesting. I saw some C# files, from which it seems it is implemented in C#. Is there going to be an implementation in Dafny?
It could be done, but what would be the virtue of it? Most programming languages are not self-hoisted for a reason.
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.