Feature request: specifying the target language parent namespace when compiling

[robin-aws]

Projects that want to embed compiled Dafny code inside libraries will frequently want to isolate the compiled code under a specific namespace. For example:

module {:extern "software.amazon.cryptography.materialproviders.internaldafny.types" } AwsCryptographyMaterialProvidersTypes

The challenge with using :extern for this is that it's not realistic to expect a single symbol to make sense for all target languages. Several suggestions have been made to allow specifying extern names per language somehow:

• Dafny 4.0 suggestion: Break up {:extern} and support language specificities #2397
• feat: enable extern declarations to be contingent on OS or target language #3030
• Dafny compiler plugin to mangle extern arguments smithy-lang/smithy-dafny#45

For the specific case of just relocating the compiled code, however, it would be a lot simpler to just provide a prefix namespace when building the code on a per-language basis. This would be adequate for smithy-dafny, since the user-facing target language symbols are generated from Smithy models instead anyway, so there is actually no need for precise control over extern attributes.

As a strawperson proposal, this could just be an option like --compile-prefix "software.amazon.cryptography.materialproviders.internaldafny", although it may be poor UX to have a single term across all languages, even if the build or configuration of a project can provide different values for each target language.