Skip to content

Conversation

@atomb
Copy link
Contributor

@atomb atomb commented Nov 5, 2025

Adds a document describing the semantics of Strata Core (consisting of Lambda and Imperative components). The document is written in Verso and imports the Strata library to allow docstrings to appear directly in the text.

Note that Strata Core is not a new dialect, but rather a new name for the combination of Lambda and Imperative. It does not yet have a concrete syntax. Concrete syntax will likely be provided through an evolution of #224, to assist in the goal of keeping Strata Core as close to B3 as possible.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

github-merge-queue bot pushed a commit that referenced this pull request Dec 9, 2025
Addresses TODO in in-progress documentation (PR #186)


By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.

Co-authored-by: Josh Cohen <cohenjo@amazon.com>
@atomb atomb marked this pull request as ready for review December 15, 2025 22:45
@atomb atomb requested a review from a team as a code owner December 15, 2025 22:45
@atomb atomb changed the title [WIP] Strata language definition doc Strata language definition document Dec 15, 2025
@aqjune-aws
Copy link
Contributor

In the hourglass image, should we have the SMT solver as a backend as well? This will help users know the SMT VCGen of Strata works. There is already CHC solver in the diagram as well.

Copy link
Contributor

@MikaelMayer MikaelMayer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Initial comments, thank you very much for doing these clarifications.

@atomb atomb enabled auto-merge December 18, 2025 20:31
@atomb
Copy link
Contributor Author

atomb commented Dec 18, 2025

In the hourglass image, should we have the SMT solver as a backend as well? This will help users know the SMT VCGen of Strata works. There is already CHC solver in the diagram as well.

Yes, we should. I made several updates to the diagram and text describing it while I was at it.

atomb and others added 3 commits December 18, 2025 12:53
It now more clearly indicates what exists and what doesn't so far.
Add handling of while loops and FloorDiv. Increase types we support for
Mult.


By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.
@atomb atomb added this pull request to the merge queue Dec 18, 2025
Merged via the queue into main with commit 22e10d7 Dec 18, 2025
16 of 17 checks passed
@atomb atomb deleted the langdef-doc branch December 18, 2025 22:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

7 participants