Skip to content

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

@robin-aws

Description

@robin-aws

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)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions