-
Notifications
You must be signed in to change notification settings - Fork 8
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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"
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
took a stab
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not sure what the purpose of this sentence is
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
An example here as well.
design/detailed-diagrams.md
Outdated
|
||
``` | ||
|
||
### Testing/Verification |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Example pls
Co-authored-by: lavaleri <[email protected]>
Co-authored-by: lavaleri <[email protected]>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Made it through the main README, will come back to the detailed diagrams. Awesome stuff so far.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
"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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This feature is used to test
smithy-dafny
on itself
in the TestModels, and is used by the Encryption SDK...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.