feat: Start adding design docs #304
Conversation
Initial overloaded Readme
design/README.MD
Outdated
| The goal is for Dafny developers | ||
| to call native AWS SDKs. | ||
|
|
||
| ### Wrapped Library |
There was a problem hiding this comment.
I'm not sure how to improve this section, but it feels like a new reader won't get the point unless they already understand how all these parts work together and the motivations for needing to set things up this way.
How I understand this in my brain:
"I have a smithy-dafny library, and I want to test one of it's APIs" ->
"I could manually write tests per runtime, but that is expensive" ->
"I could write Dafny test against one of the Dafny interfaces, but then I'm not testing any of smithy-generated code" ->
"Thus, we wrote a WrappedLibrary feature, which allows you to call a smithy-dafny library within your dafny code" ->
"Write tests in Dafny, referencing the wrapped smithy-dafny library, to get integrations tests in every language"
We sort of hit on all of these in the text below, but I don't think it's written to guide new readers. Is the point of this design to document things for those with context, or to help new readers understand why things are set up the way they are?
There was a problem hiding this comment.
I see that in a later section we do have this narrative... Unsure from a doc perspective if the narrative should be brought up here, or whether any breadcrumb can be left here to say "wait this will make sense later I promise"
design/README.MD
Outdated
| The goal is for native developers | ||
| to call Dafny libraries with idiomatic types. | ||
|
|
||
| ### Wrapped AWS Services |
There was a problem hiding this comment.
Similar to below, it might be good to prime new readers with the problem this feature is solving. e.g. "If I am writing code in Dafny and want to make a call to an AWS service, how do I do that?"
There was a problem hiding this comment.
Generate Dafny AWS SDK clients maybe? smithy-rs worded it like this: https://smithy-lang.github.io/smithy-rs/design/overview.html#code-generation
design/README.MD
Outdated
| This is where [wrapping a library](#wrapped-library) comes in. | ||
|
|
||
| We want the test in Dafny and we want to test the conversions. | ||
| by building a project we can control the implementation. |
There was a problem hiding this comment.
I'm not sure what the purpose of this sentence is
There was a problem hiding this comment.
We want to test the type conversions.
We also want to write these tests in Dafny
so that we can use these tests for every runtime.
To test the type conversions,
you would need to write them in every language.
But we do not want to write the tests in every language.
If we write a test and implementation in Dafny
we can run the conversions between these two
Dafny methods and test the type conversion.
design/detailed-diagrams.md
Outdated
| subgraph NetA["A<sub>.net</sub>"] | ||
| NetAFromDafny | ||
| NetATypes | ||
| NetAInterface | ||
| NetATypeConversion["To/From Dafny"] | ||
|
|
||
| NetATypeConversion --> NetAInterface | ||
| NetAFromDafny --> NetAInterface | ||
| NetATypes --> NetAInterface | ||
| AModel -.->|CodeGen| NetATypes | ||
| AModel -.->|CodeGen| NetAInterface | ||
| AModel -.->|CodeGen| NetATypeConversion | ||
| A ==>|Dafny Compilation| NetAFromDafny |
There was a problem hiding this comment.
This subgraph isn't making sense to me
design/detailed-diagrams.md
Outdated
| NetB["B<sub>.net</sub>"] | ||
| B ==>|Dafny Compilation| NetB | ||
|
|
||
| NetB --> NetAFromDafny |
There was a problem hiding this comment.
it's not clear, but this is saying that the "internals" of the .NET B project call into "internals" of the .NET A project?
design/detailed-diagrams.md
Outdated
|
|
||
| ``` | ||
|
|
||
| ### Extern Library Development |
design/detailed-diagrams.md
Outdated
|
|
||
| ``` | ||
|
|
||
| ### Testing/Verification |
Co-authored-by: lavaleri <[email protected]>
Co-authored-by: lavaleri <[email protected]>
design/README.MD
Outdated
| while others have either a different default or a single size. | ||
| There are also complicated types like streams. | ||
| All these languages have equivalent | ||
| but not congruent types to each other. |
There was a problem hiding this comment.
"congruent" doesn't immediately resonate for me in this context. Are you trying to point to the fact that for e.g. string in one language may allow values that it doesn't in others?
There was a problem hiding this comment.
I'm trying to distinguish between similar and congruent in terms of geometry. Like the difference between similar and congruent triangles.
When we are sloppy we talk about things bing the "same" but what we really mean is that they are similar. So every language has an Array, but not all Arrays are exactly the same.
design/README.MD
Outdated
| @@ -0,0 +1,456 @@ | |||
| ## Overview | |||
There was a problem hiding this comment.
This section is biasing a bit too much for just the polymorphing use case IMO. It's probably worth framing this as "Like any Smithy-based code generator, smithy-dafny generates Dafny code for Smithy interfaces, but there's more to it than that because Dafny supports multi-targeting" etc.
design/README.MD
Outdated
| They are not terribly opinionated | ||
| about how native project should be set up. |
There was a problem hiding this comment.
Really? :) Seems to me like the shared makefile is very opinionated about how everything is laid out.
I think this is just another issue with the ambiguity of smithy-dafny though - the repo on the whole is opinionated because it includes the shared makefile, but you're trying to say the code generation tools don't care (which I think needs to change, since we should be generating more than just the code from the Smithy models)
design/README.MD
Outdated
| `smithy-dafny` can take a smithy model | ||
| and output the generated native code anywhere. |
There was a problem hiding this comment.
I think we need to pull in the difference between the CLI and the Smithy build plugin at this point.
design/README.MD
Outdated
|
|
||
| Here is an example project structure. | ||
|
|
||
| ```mermaid |
There was a problem hiding this comment.
This one shouldn't be a diagram, just ascii art. e.g. the directory structure snippet from https://github.com/smithy-lang/smithy-typescript?tab=readme-ov-file#using-smithy-typescript-with-gradle
design/README.MD
Outdated
There was a problem hiding this comment.
top-level nit: just noticed the Smithy guide specifies designs rather than design: https://smithy.io/2.0/guides/building-codegen/creating-codegen-repo.html#codegen-repo-layout
design/README.MD
Outdated
|
|
||
| ## Definitions | ||
|
|
||
| - Runtime or native runtime: |
There was a problem hiding this comment.
i'm new to the project so might be lacking some context - but isn't "runtime" a super overloaded term? why not just call them "transpilation targets"?
design/README.MD
Outdated
| - Smithy-runtime: | ||
| The project used to generate native types | ||
| for Smithy shapes. | ||
| - Polymorph or polymorph-runtime: |
There was a problem hiding this comment.
are these synonymous? if so, any thoughts on just standardizing on "polymorph" so that usage of "polymorph-runtime" doesn't imply it's something different?
design/README.MD
Outdated
| The transformation layer between Dafny types | ||
| and native types, | ||
| e.g. polymorph-java. | ||
| - Shim: |
There was a problem hiding this comment.
even though it's a shim, would a less general term help clarify its purpose?
design/README.MD
Outdated
| for your Smithy model. | ||
| This creates a shim with native interfaces. | ||
| These native interfaces are connected | ||
| to the Dafny interface |
There was a problem hiding this comment.
just fyi - this part took me some time to digest, but that was probably due to my unfamiliarity with Dafny. e.g. "we're calling Dafny code from Rust? how?" for me, as a newcomer, it would have been clearer to have a term that clarified it was the "native but non-idiomatic code based on Dafny's typesystem / assertions" (if that's the right way to think of it).
design/README.MD
Outdated
| The first thought is be to write tests in each runtime. | ||
| But this is very expensive. | ||
| Also keeping track of all these tests across different runtimes is difficult. | ||
| You don't want to have tests only in some runtimes but not others. |
There was a problem hiding this comment.
you also wouldn't be able to implement all tests in all languages. e.g. you may want to test that a value is never null in Java, but you can't write that test against idiomatic Rust code since null doesn't exist in the language; if you want a never-null String then just write String. so tests would all have to be customized around each language's design to fill in the blanks for what their type systems do not enforce.
design/README.MD
Outdated
| By wrapping the whole project | ||
| we force an additional type conversion. |
There was a problem hiding this comment.
not sure i understand this
design/README.MD
Outdated
|
|
||
| This feature is used to test `smithy-dafny` on itself | ||
| in the TestModels. | ||
| This features is used by the Encryption SDK |
There was a problem hiding this comment.
This feature is used to test
smithy-dafnyon itself
in the TestModels, and is used by the Encryption SDK...
There was a problem hiding this comment.
what is the Encryption SDK? it hasn't been mentioned until now. i see its mentioned later in an example. it sounds like this is just giving an example of a client which is doing this, but not sure if adding this extra section helps to clarify anything.
Co-authored-by: Robin Salkeld <[email protected]>
Co-authored-by: Robin Salkeld <[email protected]>
Co-authored-by: Robin Salkeld <[email protected]>
Co-authored-by: Robin Salkeld <[email protected]>
Co-authored-by: Robin Salkeld <[email protected]>
Co-authored-by: Robin Salkeld <[email protected]>
There was a problem hiding this comment.
I'm super happy to get this added, and although I do want to take another pass at it and/or add more detail here or somewhere else, it's just so much better to have merged than sitting here. In that spirit I'm gladly approving even though I will likely cut a PR to improve even further relatively soon.
Thanks so much for taking the time on this!
Initial overloaded Readme
I will also add a few other diagrams.
We can break up this file as needed.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.