The current approach for connecting Dafny code to code in other target languages is to add {:extern} to various program elements, and write additional target language shim code to connect what the Dafny code generators spit out to existing or freshly-written code.
There are a number of issues with this approach:
The target language shim code inevitably refers to internal datatypes from the Dafny runtime, which frequently change within major versions.
Having a single {:extern} attribute name creates the false impression that a single {:extern} declaration can be expected to work for all target languages.
Different languages have different concepts and different restrictions on symbols. For example, in Java and C# {:extern "a.b.c"} can be used on a module to specify the package or namespace for the module, but this is not allowed in Go since it does not allow dots in package names.
The arguments to {:extern} are completely unconstrained/untyped, leading to hacks of embedding whole chunks of target language code instead of just symbols as intended (looking at you @MikaelMayer :) ), and hence a lack of encapsulation for any future optimizations.
It is not intuitively clear what the meaning of the one or two arguments to the attribute mean, since they are interpreted differently by different backends.
There is a lack of distinction between {:extern} used to mean "this is externally implemented" (and hence body-less definitions are allowed) vs. "this is referenced externally". Again different backends may not agree on which is which.
It is difficult to figure out what name and signature the externally implementation needs to conform to. The best option is to attempt to compile/run the incomplete program and guess at this from the resulting errors.
We're in the current state mostly because {:extern} grew organically as Dafny gained compilation at all, and then multiple compilation targets. We need to step back and design a better approach. This will likely result in a new set of attributes per target language to support accurately binding Dafny symbols/types to existing code features, such that Dafny code generation is always sound under the assumption these bindings are accurate.
To ensure we don't overfit the general approach to a particular language, we can focus on Java and Rust together at first, as two important and very different target languages.
To further bound the initial scope, the new approach should at least handle the simple and aggregate Smithy types supported by smithy-dafny.
The current approach for connecting Dafny code to code in other target languages is to add
{:extern}to various program elements, and write additional target language shim code to connect what the Dafny code generators spit out to existing or freshly-written code.There are a number of issues with this approach:
{:extern}attribute name creates the false impression that a single{:extern}declaration can be expected to work for all target languages.{:extern "a.b.c"}can be used on a module to specify the package or namespace for the module, but this is not allowed in Go since it does not allow dots in package names.{:extern}are completely unconstrained/untyped, leading to hacks of embedding whole chunks of target language code instead of just symbols as intended (looking at you @MikaelMayer :) ), and hence a lack of encapsulation for any future optimizations.{:extern}used to mean "this is externally implemented" (and hence body-less definitions are allowed) vs. "this is referenced externally". Again different backends may not agree on which is which.We're in the current state mostly because
{:extern}grew organically as Dafny gained compilation at all, and then multiple compilation targets. We need to step back and design a better approach. This will likely result in a new set of attributes per target language to support accurately binding Dafny symbols/types to existing code features, such that Dafny code generation is always sound under the assumption these bindings are accurate.To ensure we don't overfit the general approach to a particular language, we can focus on Java and Rust together at first, as two important and very different target languages.
To further bound the initial scope, the new approach should at least handle the simple and aggregate Smithy types supported by smithy-dafny.
Relevant issues for background: https://github.com/dafny-lang/dafny/issues?q=is%3Aopen+is%3Aissue+label%3A%22area%3A+ffi%22