Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Discourage clients from referencing Dafny-compiled C# code #244

Closed
robin-aws opened this issue Mar 30, 2020 · 1 comment
Closed

Discourage clients from referencing Dafny-compiled C# code #244

robin-aws opened this issue Mar 30, 2020 · 1 comment

Comments

@robin-aws
Copy link
Contributor

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)

@robin-aws robin-aws added this to the Public Beta milestone Mar 30, 2020
@farleyb-amazon farleyb-amazon removed this from the Public Beta milestone May 5, 2022
@seebees
Copy link
Contributor

seebees commented Jun 14, 2022

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.

@seebees seebees closed this as completed Jun 14, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants