Dafny 4.0 suggestion: Break up {:extern} and support language specificities

[MikaelMayer]

Currently, the annotation {:extern} and {:compile false} are used intertwined in three different cases

• {:extern "newName"} Here is how this method, module or function name should be compiled and accessed externally (this is what we export)
• {:extern} This method or function is defined externally, here is their signature, don't compile it. (this is what we import)
• {:extern "newName"} {:compile false}: this weird case is that, if we want to import a method or function with a different Dafny name that the real name, we need to use the export syntax but indicate we are not compiling it. Why we are not compiling it? It's not primarly because we want to deactivate compilation. It's because we want to import the definition.

My point is, it looks like hot and cold taps: We all want to adjust temperature and pressure independently, not the individual amounts of hot and hold. In our case, "hot" is {:extern} and "cold" is {:compile false}, and "temperature" is "I want to import this from external Dafny code" and "pressure" is "I want to export this". Moreover, in both cases, we want to be able to specify language-specific names.

Here is my breaking proposal for Dafny 4. We get rid of the existing {:extern [[<string>,] <string>]} and {:compile false}, and instead rely on two new attributes {:compile <string>} and {:import [[<string>,] <string|map<string,string>>]}, like this:

• {:compile "name"} At the time of compilation, replaces Dafny's symbol by "name" at definition site and at call site. Should work for any language. Previously {:extern "name"}.
• {:compile map["csharp" := "name"]} Same as before, except that we can associate a name for every language, and fail if the compile target does not support that language. Did not exist previously.
• {:import} to import an existing external symbol in Dafny with the same name. Should work for any language. Previously {:extern} (which has an implicit {:compile false}).
• {:import "F"} to import the existing external symbol F in Dafny, overriding Dafny's symbol "name". Should work for any language. Previously {:extern "F"} {:compile false}.
• {:import map["csharp", "name"]} same as before, except we restrict the languages target from which we can import the symbol "name". Did not exist previously.
• {:import "Module", "F"} to import the existing external symbol Module.F in Dafny. Should work for any language. Previously {:extern "Module", "F"} {:compile false}.

[seebees]

I like the name changes.
Why can I not {:compile "Module", "name"}?

While I can see some benefit for {:compile map["csharp" := "name"]} this adds a lot of complexity. How would you see using this?

{:import map["csharp", "name"]} I do not believe that the same function exists in different runtimes with different names, but the same "signature". Do you have an example?

[cpitclaudel]

I have no strong feelings, but we should be careful to not create more confusing terminology do we know other languages that use "export" and "import" in this sense?

C uses extern like Dafny (to prevent a name from being mangled), and uses the absence of a body for what we call {:compile false}.

For me the main issue with Dafny's extern/compile attributes today is that {:extern} sometimes implies {:compile false}, and sometimes doesn't, depending on which kind of entity it is applied to.

[robin-aws]

Related prior discussion: #469

[robin-aws]

I agree the FFI badly needs an overhaul in general. Another aspect you don't mention is the common use case, not directly supported at all, of wanting to expose a Dafny-idiomatic signature as a target language-idiomatic signature (e.g. mapping a Dafny string to a java.lang.String instead of a Dafny.Sequence<Character>).

Given this is a highly complex design space, I'd prefer not to rush getting it right so that it can make the Dafny 4.0 train. It looks like we're leaning towards fresh terms and deprecating the existing ones anyway, which we can do with deprecation and doesn't require an immediate major version bump.