Extern V2 for Java and Rust - design #5784
Labels
area: ffi
The {:extern} attribute and otherwise interfacing with code in other languages
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve 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
The text was updated successfully, but these errors were encountered: