You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The output of the Dafny-to-C# compiler does not currently attempt to encapsulate or hide any methods or state, and it is not that obvious which pieces are intended to be part of the public API. As we move more of the shim into Dafny code itself, we shouldn't be relying on the rule of ".NET customers should only refer to the hand-written C# interfaces and datatypes". To complement the efforts to ensure the interface between Dafny and external code is sound (#165), we should also at least clearly document which code elements are part of that API and which aren't.
One possibility is modifying Dafny itself to add something like "__DAFNY_INTERNAL__" to all names that that the Dafny compiler spits out, so that even if they are publicly addressable in C# code it will be fairly obvious that client code should not reference such elements. We could also investigate flagging them as deprecated somehow, but that may generate a lot of noise when we later support separate compilation of Dafny projects (dafny-lang/dafny#501)
The text was updated successfully, but these errors were encountered:
Since every Dafny project is going to have such a problem
I think that this is more likely to be solved in Dafny proper.
It is already work to find and reference these symbols.
The output of the Dafny-to-C# compiler does not currently attempt to encapsulate or hide any methods or state, and it is not that obvious which pieces are intended to be part of the public API. As we move more of the shim into Dafny code itself, we shouldn't be relying on the rule of ".NET customers should only refer to the hand-written C# interfaces and datatypes". To complement the efforts to ensure the interface between Dafny and external code is sound (#165), we should also at least clearly document which code elements are part of that API and which aren't.
One possibility is modifying Dafny itself to add something like "__DAFNY_INTERNAL__" to all names that that the Dafny compiler spits out, so that even if they are publicly addressable in C# code it will be fairly obvious that client code should not reference such elements. We could also investigate flagging them as deprecated somehow, but that may generate a lot of noise when we later support separate compilation of Dafny projects (dafny-lang/dafny#501)
The text was updated successfully, but these errors were encountered: