o
odin.langpkg.dev
packages / library / syntact

syntact

4494e94library

A scope-based programming language where execution is explicit reduction.

No license · updated 2 weeks ago

Syntact

A language where everything is a scope, nothing is a function, and execution is just reduction.


Syntact is an experimental general-purpose programming language built around one primitive: the scope.

A scope is complete structured data. It can contain bindings, defaults, productions, constraints, patterns, handlers, and other scopes. It can be inspected, carved, matched, expanded, and collapsed. It is not a function, an object, a class, a struct, a module, a record, or an instance — although it can replace all of them.

The central idea is this:

Programming languages usually split programs into data, blueprints, and functions. Syntact keeps one world: data.

In most languages, runtime values live in one world, classes and structs live in another, and functions live in a third. Then the language needs bridges: constructors, methods, interfaces, traits, generics, macros, reflection, imports, dependency injection, code generation, and frameworks.

Syntact treats that split as unnecessary. There is one algebraic object — the scope — and a small set of operations over it.

A function-like computation is a scope that can be collapsed. A type is a scope used as a shape. An instance is a scope constrained or carved from another scope. A module is a scope expanded into another scope. A macro-like transformation is just ordinary manipulation of a scope before collapse.

The keystone is default completeness:

Every scope is complete by default.

A scope is not waiting for arguments. A shape is not waiting to be instantiated. A computation is not waiting to be called. Defaults make every scope real data immediately.

square -> {
  n -> 0
  -> n * n
}

square.n         // 0
square!          // 0
square{n -> 5}!  // 25

square5 -> square{n -> 5}
square5.n        // 5
square5!         // 25

square is not a function. n is not a parameter. square{n -> 5}! is not a call.

square is a complete scope with a default binding n -> 0 and a production -> n * n. square{n -> 5} derives a new scope. ! collapses that scope through its production.

What other languages express as a function call, Syntact expresses as two independent operations:

carving  derive a new scope
collapse reduce a scope through its production

That separation is the root of the language.


Syntact in one sentence

Syntact is a structural reduction language with nominal effects.

Its central claim is not that functions, types, modules, and objects are the same thing. Its claim is that they do not need to be primitive categories. They can emerge from operations over complete structures.


How to read Syntact

Syntact intentionally uses familiar surface syntax.

A beginner may read:

square -> {
  n -> 0
  -> n * n
}

square{n -> 5}!

as something close to:

function square(n = 0) { return n * n }
square(5)

That reading is useful, but incomplete.

The structural reading is:

square        a complete scope
n -> 0        a binding occurrence with a default
{n -> 5}      a structural derivation of the scope
!             explicit collapse through the scope production

Syntact is designed so shallow readings are productive, but deeper readings reveal the actual model.

A scope is not a function, object, module, record, class, or type. Those are projections produced by operations over scopes.

Classical reading vs Syntact reading

Surface form Classical temptation Syntact meaning
n -> 0 variable assignment binding occurrence
-> x return production
square{n -> 5} function call setup structural derivation
square! call/eval collapse
Point:p declaration of variable p binding colored by Point — the constraint propagates structurally
box.x field access projection through current view
Log -< e {...} callback/listener nominal effect handler
value >>- Change mutable variable resonant binding driven by nominal event
value -<< e.value assignment resonant update inside handler
x >>= expr computed property reactive derived binding
=<< expr reactive effect reactive production

The analogies in the middle column help you start reading code. They are not what the language actually does.


Core rules

  1. A scope is an ordered structure, not a symbol table.
  2. A binding is an occurrence, not a variable slot.
  3. A name is a projection, not an identity.
  4. Access resolves a name through the current view.
  5. Carving derives a new scope by targeting existing structural occurrences.
  6. A scope is closed: carving refines existing bindings, it never adds new ones.
  7. Collapse reduces a scope through its production.
  8. Shapes are scopes used as structural constraints.
  9. Patterns are scopes used analytically.
  10. Effects are nominal; everything else is structural.
  11. Defaults compose structurally.
  12. No binding is ever mutated by the core language.

Come back to this list when a section feels surprising. Most surprises resolve to one of these rules.


Status

Syntact is in active development.

The bootstrap compiler is written in Odin and runs the full pipeline end to end: parse → analyze (constraint folding) → reduce → bytecode → native x86-64 ELF. A Syntact program compiles to a runnable static executable. The analyzer proves constraints from value ranges (there is no type system, only structural coloring); the reducer collapses everything reducible — carving, collapse, references, patterns, and affine arithmetic — to a minimal form; a target-neutral bytecode then feeds an optimizing x64 backend (linear-scan allocation, register coalescing, LEA-based instruction selection, width-correct 32-bit arithmetic). An LSP (diagnostics, hover, go-to-definition, rename, completion) and six declarative test suites are part of the project.

This README describes the design direction of the language, including features that are planned but not yet implemented. The implementation plan near the end separates the working core from later layers such as events, resonance, full scope algebra, and proofs.


Why Syntact exists

Modern programming often feels more complicated than the problems it is trying to solve.

We build abstractions, then write boilerplate to work around them. We create encapsulation, then add reflection to inspect it. We write types, then write serializers, validators, schemas, mappers, builders, adapters, mocks, and dependency containers around them. We use high-level frameworks, then hope the compiler removes the overhead.

Syntact starts from a different assumption:

Many programming concepts are not fundamentally different. They are different projections of structured data and reduction.

Instead of adding another abstraction layer, Syntact tries to remove the artificial categories underneath.

The basic vocabulary is small:

scope      complete structured data
binding    directed relation inside a scope
production what a scope yields when collapsed
carving    derivation of existing structure
shape      scope used as constraint
pattern    shape used analytically
collapse   explicit reduction
handler    scoped interpretation of a nominal effect
resonance  explicit state driven by nominal events
reactivity implicit derived binding that tracks its dependencies

The syntax is intentionally familiar. Braces, dots, arrows, and names should not make the language look alien. But the semantics are different.

{...} is not just a block.

-> is not assignment.

: is not merely a type annotation. It is structural coloring that propagates implicitly.

? is not just a conditional.

! is not general evaluation.

The surface is approachable; the ontology is different.


The problem with functions

Syntact removes the function as a primitive because a function is not really primitive. It is a bundle of several ideas:

parameterization
environment
body
evaluation
calling convention
capture
effects
return
time

Most languages start with that bundle, then add features to recover the pieces: closures, lambdas, generics, async functions, iterators, traits, monads, effect systems, macros, partial evaluation.

Syntact decomposes the bundle directly:

parameterization -> carving
environment      -> scope
relation         -> binding
execution        -> collapse
effect           -> event + handler
mutation         -> resonance
reactivity       -> reactive bindings

So “no functions” is not the goal. It is the consequence of choosing smaller primitives.


Table of contents


First program

A complete Syntact program can be one line:

-> 0

The file is a scope. The production -> 0 says that the file-scope produces 0. Running the program means collapsing the file-scope.

A slightly larger program:

greeting -> "hello"
answer -> 42
-> answer

This program produces 42. The binding greeting is never used, so there is no reason for it to appear in the final binary.

For example, compiled for Linux x86-64, the resulting program can be as small as:

_start:
    mov     edi, 42         ; exit code = 42
    mov     eax, 60         ; syscall: exit
    syscall

No string "hello" remains. No hidden runtime is needed. The compiler reduced the program to what it actually does.


Scopes

A scope is what {...} creates.

point -> {
  x -> 10
  y -> 20
}

point.x // 10
point.y // 20

Scopes can nest:

user -> {
  name -> "Alice"
  address -> {
    city -> "Toulouse"
    zip -> 31000
  }
}

user.address.city // "Toulouse"

A scope is a complete ordered structure. You can bind it to a name, read its bindings, derive it, constrain values by it, match against it, expand it, or collapse it if it has a production. The role it plays — value, type, module, function-like computation, instance — comes from the operation applied to it, not from a built-in category.

A file is a scope. A folder is a scope. A library is a scope. A primitive type is a scope. A pattern can be a scope. A program is a scope.


Bindings

-> is the basic binding arrow.

name -> "Alice"
age -> 29

Read it as “name points to Alice” and “age points to 29”.

Bindings are top-down. A binding can use what exists above it in the same scope or in an enclosing scope.

x -> 1
y -> x + 1 // valid

This is invalid:

y -> x + 1 // invalid: x does not exist yet
x -> 1

A scope is not an unordered namespace. It is a directed structure. Later bindings may depend on earlier bindings. Reduction follows that structure.

This matters because there is no separate parameter zone. What other languages call a parameter is usually just an earlier binding with a default.

square -> {
  n -> 0
  -> n * n
}

n is a binding. The production can use it because it appears above.


Same-name bindings are not redeclarations

In a scope, two bindings can share a name. They are not in conflict and the second does not overwrite the first.

box -> {
  x -> 1
  y -> x
  x -> 2
}

box contains two distinct bindings, x#0 and x#1. They are independent entries in an ordered structure, not conflicting entries in a symbol table. The compiler tracks them by index.

This is not shadowing and not redefinition. It is a structural feature: a scope is a sequence of bindings, and several can share a name. Syntact treats a scope as data, not as a symbol table. A symbol table forces unique names. Data does not.

Access and carving target different occurrences

Same-name bindings introduce a subtle but central rule: access by name and carving do not look at the scope the same way.

  • Access (box.x) returns the last visible occurrence of x. It is a current-view resolution, walking the scope top-down and keeping the last one.
  • Carving (box{x -> ...}) targets the first structural occurrence of x by default. It is a structural transformation of the scope's foundation.

So given the box above:

box.x // 2          (last occurrence: x#1)
box.y // 1          (y was bound to x#0, the x in scope at that line)

And a carve:

box2 -> box{x -> 10}

box2.x // 2         (still reads the last x, which is x#1, untouched)
box2.y // 10        (y depends on x#0, which was carved to 10)

Either occurrence can be targeted explicitly:

box{x#0 -> 5}  // carve the first x
box{x#1 -> 9}  // carve the last x
box{x   -> 7}  // unqualified: carves x#0

A motivating example:

Config -> {
  port -> 8080
  url  -> "localhost:" + port
  port -> 3000
}

Config.port // 3000              (last port)
Config.url  // "localhost:8080"  (url was built from the first port)

DevConfig -> Config{port -> 9000}

DevConfig.port // 3000
DevConfig.url  // "localhost:9000"

This is not an inconsistency. The two operators answer different questions:

  • reading asks what is the current view of this name;
  • carving asks what is the structural source this scope is built on.

Same-name bindings let you expose one value through the visible name while keeping the foundational value carvable. Shadowing and structural rewriting coexist instead of fighting each other.


Productions

A production is a binding without an explicit left side.

greeting -> "hello"
-> greeting

The implicit source is the enclosing scope itself. The scope points itself at the value it produces.

This replaces return.

add -> {
  a -> 1
  b -> 2
  -> a + b
}

The scope add produces a + b when collapsed.

A scope may have several productions.

BoolLike -> {
  -> false
  -> true
}

The first production is the default. Additional productions are potentialities. This is what later allows sum-like shapes and pattern matching.


Collapse

Collapse is written !.

two -> {
  a -> 1
  b -> 1
  -> a + b
}

two.a // 1
two.b // 1
two!  // 2

! does not mean “evaluate this expression”. It specifically means: reduce this scope through its production.

A binding may point directly to a value:

box -> {
  x -> 1
  y -> x + 1
}

box.y // 2

Here y is not a scope, so there is nothing to collapse.

A binding may also point to a scope:

box -> {
  x -> 1
  y -> {
    -> x + 1
  }
}

box.y  // the scope bound to y
box.y! // 2

The rule is:

expressions resolve
scopes collapse

A scope with no production collapses to none.

empty -> {
  x -> 1
  y -> 2
}

empty! // none

Collapse is intentional. It happens where ! appears. That explicitness is what lets the compiler reduce as much as possible before runtime.


Execution patterns

! is the basic collapse operator, but collapse can be wrapped by execution patterns.

An execution pattern says how a collapse should happen, without changing the scope being collapsed.

Basic patterns:

!   sequential collapse
<>  threading
[]  parallel CPU
()  background
||  GPU

These patterns compose around !.

result -> work!       // sequential
result -> work<!>     // collapse on another thread
result -> work[!]     // collapse in parallel on CPU
result -> work(!)     // collapse in background
result -> work|!|     // collapse on GPU

The important part is that execution strategy belongs to the collapse site, not to the computation itself.

work does not have to be declared as async, threaded, parallel, background, or GPU-aware. The same scope can be collapsed differently in different contexts.

result -> packed<[!]>     // threaded parallel execution
result -> packed([<!>])   // parallel threaded execution
result -> packed<(!)>     // threaded background execution
result -> packed(<!>)     // background threaded execution
result -> packed<|!|>     // threaded GPU execution
result -> packed(|!|)     // background GPU execution

Patterns may be nested arbitrarily as long as the composition is valid for the scope being collapsed.

result -> packed(<[!]>)    // background threaded parallel execution
result -> packed(|<[!]>|)  // GPU background threaded parallel execution
result -> packed([([!])])  // parallel background parallel execution

Execution patterns are not special function calls. They are collapse forms.

They can be applied to carved scopes:

map{list -> {1 2 3 4 5} mapper -> double}![!]
reduce{list -> packed! reducer -> add}<!>
transform{shape -> shape transformer -> double}(<[!]>)

They can also be applied to other reducible expressions where the result is meaningful:

Circle{radius -> 10}<[!]>
(1 + 2)<!>
map{list -> {2 3}}[!] + reduce{reducer -> plop}<!>

The compiler is responsible for checking whether a pattern is legal. For example, parallel CPU or GPU collapse may require purity or effect handlers compatible with that execution mode. A scope that emits unsafe effects cannot simply be sent to a parallel or GPU collapse unless the surrounding handlers make that legal.

This keeps concurrency, background work, threading, and GPU dispatch out of the computation itself. They are not different function kinds and do not require separate async syntax. They are different ways to collapse the same scope.

Patterns constrain strategy, not machine form

A GPU collapse does not mean “compile this scope into exactly one GPU kernel”.

Depending on the reduced structure, a GPU collapse may produce:

zero kernels       if everything is reduced at compile time
one kernel         for simple data-parallel work
multiple kernels   for reductions or complex pipelines
library calls      for specialized operations such as matrix multiplication
a compile error    if the region is not legal for GPU execution

|!| constrains the collapse strategy. It does not expose a kernel model in the source language. The same is true of [!], <!>, and (!): they declare a strategy, not a fixed lowering.


Carving

{...} applied to an existing scope carves a derived scope.

Point -> {
  x -> 0
  y -> 0
}

shifted -> Point{x -> 5}

Point.x   // 0
shifted.x // 5
shifted.y // 0

Carving does not mutate the original. It derives a new scope.

Carving propagates through dependent bindings.

box -> {
  x -> 1
  y -> x + 1
}

box.y // 2

box2 -> box{x -> 10}
box2.y // 11

This is why carving is not argument passing. A function call passes values into a fixed body. A carve derives a new structure before reduction happens.

square -> {
  n -> 0
  -> n * n
}

square{n -> 5}! // 25

Read it as:

derive square with n = 5
then collapse the derived scope

Carving is closed

Carving refines existing structure. It never adds new structure.

A scope is closed: its set of bindings is fixed the moment it is written. Carving can target any binding that already exists and derive a new scope with a different value, but it cannot introduce a binding that was not there.

Role -> {
  -> "member"
  -> "admin"
}

User -> {
  String:name
  u8:age
  Role:role -> "member"
}

AdminUser -> User{
  role -> "admin" // refines the existing `role` binding
}

Targeting a name that does not exist is an error, not a silent addition. This protects the algebra: a typo cannot quietly grow a scope.

User{
  raole -> "admin" // error: `raole` is not a binding of User
}

If you need a different shape, you write a different scope. A scope is complete and closed: you carve what is there, you do not bolt on what is not.

{...} means derivation or refinement of existing structure. There is no extension operator — there is no way to add a binding to an existing scope.


Defaults and completeness

Defaults are not a small convenience feature. They are what make the one-world model possible.

A scope is complete because its bindings have defaults. A shaped binding is complete because its shape has a default. A computation is complete because it can be inspected or collapsed without being called.

Point -> {
  u8:x
  u8:y
}

Point:p

p.x // 0
p.y // 0

Point is not a blueprint waiting for construction. It is already a complete scope.

Point.x // 0
Point.y // 0

You can derive a specific point:

p -> Point{x -> 10 y -> 20}

You can constrain a binding by it:

Point:p{x -> 10 y -> 20}

You can inspect it:

p.x

The difference between “type”, “value”, “blueprint”, and “instance” is not a difference of world. It is a difference of operation.

Defaults compose

Defaults are compositional.

The default of a structured scope is obtained from the defaults of its shaped bindings. A complete structure composed of complete parts is itself complete.

Vec2 -> {
  f32:x
  f32:y
}

Transform -> {
  Vec2:position
  Vec2:scale -> Vec2{x -> 1 y -> 1}
}

Transform.position.x // 0
Transform.position.y // 0
Transform.scale.x    // 1
Transform.scale.y    // 1

Defaults are not magic values produced by the compiler. They are the natural reading of a complete structure.


No null, no uninitialized state

Syntact has no null.

There is no hidden “missing value” state and no uninitialized binding. A binding is complete because its shape provides a default, and defaults compose structurally.

Point -> {
  u8:x
  u8:y
}

Point:p

p.x // 0
p.y // 0

p is not partially initialized. It is complete by composition.

If absence, failure, optionality, or emptiness is needed, it must be modeled structurally. It is never smuggled in as a null pointer or an uninitialized value.


Algebraic immutability

This is the most important property of Syntact, and it must not be confused with the way mainstream languages talk about “immutability”.

Nothing is ever modified. A scope, once described, never changes. Every operator that looks like it changes something actually derives a new scope. The original is untouched and remains valid.

box -> {
  x -> 1
  y -> x + 1
}

box2 -> box{x -> 10}

box2 is not box with x patched. box2 is a new scope derived from box by carving. In box, x is 1 and y is 2. In box2, x is 10 and y is 11. Both scopes coexist. Neither was mutated.

This is not “immutability by convention”. It is the meaning of carving. There is no operator in the language that mutates a binding in place. Every transformation is a fresh derivation in the algebra.

A consequence: there is no notion of “the value of x after we changed it”. There is only box.x, box2.x, and any other scope that participates in the derivation graph. Any of them can be inspected at any time.


Mutation and reactivity are opt-in

Because the algebra is immutable, ordinary bindings cannot be mutated, reassigned, or updated in place. There are two separate mechanisms to model change, both layered on top of the immutable core:

  • Resonance (>>- / -<<): explicit state driven by nominal events. A binding is declared resonant and its value evolves only when a named event is emitted and handled.
  • Reactivity (>>= / =<<): implicit derived bindings that automatically recompute when their dependencies change. No explicit event is needed.

Resonance is the foundation: it is where mutation actually happens. Reactivity is built on top: a reactive binding observes other bindings (including resonant ones) and recomputes structurally.

A program with no resonant or reactive bindings is purely algebraic. Combined with the no-null rule above, this gives the core a strong guarantee: every binding has a value, no value is ever silently replaced, and the only way to model change is to opt in explicitly.


Primitive types

Primitive types are scopes known by the compiler.

They are primitive in representation, not in ontology.

A minimal primitive set may include:

none      empty value sentinel
bool      false or true
u8        unsigned 8-bit integer
i8        signed 8-bit integer
u16       unsigned 16-bit integer
i16       signed 16-bit integer
u32       unsigned 32-bit integer
i32       signed 32-bit integer
u64       unsigned 64-bit integer
i64       signed 64-bit integer
usize     architecture-sized unsigned integer
isize     architecture-sized signed integer
f32       32-bit floating point
f64       64-bit floating point
char      character / scalar value
String    string data

u8 is the shape of unsigned 8-bit values, defaulting to 0.

bool is the shape of false and true, defaulting to false.

String is the shape of strings, defaulting to "".

u8:count       // 0
bool:enabled   // false
String:name    // ""

The exact primitive set may evolve, but the rule should not: primitives behave like scopes in the language model.


Shapes

: constrains a binding by a shape.

u8:age
String:name
Point:p

Read u8:age as “age shaped like u8”.

A shaped binding can receive a value:

u8:age -> 29
String:name -> "Alice"

or use its default:

u8:age      // 0
String:name // ""

A shaped binding can be carved immediately:

Point:p{x -> 10 y -> 20}

This means:

create p
constrain p by Point
carve p with x -> 10 and y -> 20

: is not just documentation. It changes how the binding is checked and completed.

A scope used with : is interpreted as a shape. The same scope used with ! is collapsed. The same scope used with {...} is carved.

The object is the same. The operator selects the operation.

Anonymous shaped bindings

The name can be omitted.

Circle:

This means “an anonymous binding shaped like Circle”. It is especially useful in patterns and structural definitions.

Shape -> {
  -> Circle:
  -> Square:
}

This says that a Shape can produce a Circle or a Square.

Constraints as implicit structural coloring

: does more than check a value against a shape. It colors the binding structurally: every constraint imposed by the shape propagates through the binding and everything it contains, without needing to be restated.

Any scope can be used as a constraint. Primitive types, user-defined scopes, carved scopes, refined scopes — the mechanism is the same.

Array -> {
  T -> {}
  -> {}
  -> {T: ...Array:}
}

Array is a recursive scope parameterized by T. Its productions describe either an empty scope or a head shaped by T followed by more Array.

Now define a union-like scope:

F32OrString -> {
  -> f32:
  -> String:
}

F32OrString is a scope whose productions are either f32 or String. It is not a type declaration — it is a scope that produces one of two shapes.

Use it as a constraint through carving:

Array{F32OrString}:array -> {0.1 2.0 "hello"}

What happens here:

Array{F32OrString}    carve Array with T = F32OrString
:array                constrain array by the carved scope
-> {0.1 2.0 "hello"}  give it a value

The constraint on array is Array{F32OrString}. This means every element must satisfy F32OrString. But this constraint was never written on any individual element. 0.1 is not annotated as f32:. "hello" is not annotated as String:. The coloring is implicit — it flows from the constraint on the whole scope down to each structural position.

This is a direct consequence of default completeness and the scope model. A constraint is not an annotation that lives on one binding. It is a structural property of the scope, and it propagates inward.

If array is later passed to another scope that expects Array:, the F32OrString constraint on T travels with it. No re-annotation is needed at the receiving site.

printAll -> {
  Array:items
  -> items ? {
    {} -> "done"
    {head ...tail} -> head + " " + printAll{items -> tail}!
  }
}

printAll{items -> array}!

printAll accepts any Array:. Because array was colored as Array{F32OrString}, the constraint is already satisfied. The coloring is carried by the value, not by the call site.

This is not type inference in the traditional sense. There is no separate type system reconstructing constraints from usage. Coloring is a structural property: once a scope is constrained, every operation that depends on it inherits the constraint. The scope carries its coloring the way data carries its shape.


The pattern operator ?

? is the pattern operator.

It takes a value on the left and a set of patterns on the right. The first matching pattern selects the corresponding production.

The simplest patterns are literal patterns:

n ? {
  0 -> "zero"
  1 -> "one"
  -> "many"
}

The final branch has no explicit pattern. It is the default branch.

A pattern can be a shape:

shape ? {
  Circle: -> "circle"
  Square: -> "square"
  -> "unknown"
}

Here Circle: means “matches the Circle shape anonymously”.

A pattern can be a refinement:

n ? {
  0 -> "zero"
  >0 -> "positive"
  -> "negative"
}

A pattern can be composed:

value ? {
  (u8 | i8) & >10 -> "small signed-or-unsigned int greater than 10"
  -> "something else"
}

This is why ? is not just an if/switch replacement. It is the analytic side of the algebra.


Destructuring patterns

Patterns can destructure.

Circle -> {
  u8:radius
}

area -> {
  Shape:shape

  -> shape ? {
    Circle:{radius(r)} -> r * r * 3
  }
}

Circle:{radius(r)} means:

match a Circle
open its structure
extract radius
capture radius as r
make r available on the right side

You can refine while destructuring:

shape ? {
  Circle:{radius(r)?<10} -> r * r * 3
  Circle:{radius(r)}     -> r * r * 3
}

You can unify different shapes through a common projection:

Square -> {
  u16:side
}

Diamond -> {
  u16:side
}

area -> {
  Shape:shape

  -> shape ? {
    Square:{side(s)} | Diamond:{side(s)} -> s * s
  }
}

No nominal interface is required. The pattern says what structure it needs.


Carving versus destructuring

This distinction is important.

These three forms are different:

Circle:{radius?<10}
Circle{radius?<10}
Circle{radius?<10}:

Circle:{...}

This is shape constraint plus local destructuring or patterning.

Circle:{radius(r)?<10} -> r

It creates an anonymous value constrained by Circle, inspects its radius, captures it as r, and checks r < 10.

The capture exists in the branch or scope where the pattern is used.

Circle{...}

This carves or refines the scope Circle itself.

SmallCircle -> Circle{radius?<10}

This defines a refined shape. It does not capture radius into a local name.

Circle{...}:

This creates an anonymous binding constrained by the carved shape.

Circle{radius?<10}:

This means “some anonymous value shaped like a Circle whose radius is less than 10”. It still does not create a local r unless you destructure it.

To get r:

SmallCircle -> Circle{radius?<10}

SmallCircle:{radius(r)} -> r * r * 3

This separation keeps the syntax algebraic instead of magical.


Scope algebra

Syntact is meant to be an algebra of scopes, not merely a language with algebraic data types.

The same operators should apply to values, shapes, patterns, modules, refinements, grammars, and eventually proofs.

Examples:

Positive -> >0
Small -> <100

PositiveU8 -> u8 & Positive
SmallPositiveU8 -> u8 & Positive & Small

weirdInt -> (u8 | i8) & >10

Direct use:

((u8 | i8) & >10):x -> 42

Domain shapes:

Port -> u16 & >0
Percent -> u8 & <=100
AdultAge -> u8 & >=18 & <=120

Refined structures:

Circle -> {
  u8:radius
}

SmallCircle -> Circle{radius?<10}
MediumCircle -> Circle{radius?(>=10 & <50)}
BigCircle -> Circle{radius?>=50}

Structural override:

Role -> {
  -> "member"
  -> "admin"
}

User -> {
  String:name
  u8:age
  Role:role -> "member"
}

AdminUser -> User{
  role -> "admin"
}

The goal is closure: construction, derivation, matching, destructuring, refinement, and expansion should be explained by the same algebra, not by separate feature systems.

Grammars as shapes

String patterns and grammars should also live in the algebra.

alpha -> 'a'..'z' | 'A'..'Z'
digit -> '0'..'9'
emailChar -> alpha | digit | '.' | '_' | '-'

Email -> {
  String:(s) -> "email@example.com"

  -> s ?!
    emailChar*1..
    + '@'
    + emailChar*1..
    + '.'
    + alpha*2..
}

The long-term idea is that regex-like validation is not a string passed to a library. It is a grammar-shaped constraint in the language algebra.

Another example:

idChar -> 'a'..'z' | 'A'..'Z' | '0'..'9' | '_' | '-'

Identifier -> {
  String:(s) -> "defaultId"

  -> s ?!
    idChar*1..
    & ~(.. + '_')
}

Then:

Identifier:id                 // defaultId
Identifier:someId -> "someId" // ok
Identifier:oops -> "bad_"     // rejected if statically known/provable

This is not meant to be in the first implementation. But it shows the direction: data modeling, parsing, validation, and proofs should not be separate worlds.


Pull bindings and genericity

<- declares a hole filled by the use site.

identity -> {
  T <- none
  value <- none
  -> value
}

identity{value -> 5}!
identity{value -> "hello"}!

T and value are both holes. Carving with value -> 5 fills value, and T is inferred from the shape of what filled it. The use site never has to mention T — it is recovered from the carving.

A hole can also be filled explicitly. Since a hole is pulled, not pushed, the fill arrow at the use site is <-, not ->:

identity{T <- u8 value -> 5}!

value -> 5 is an ordinary push binding into the hole value. T <- u8 says “fill the hole T with u8”. Mixing the two arrows is not a quirk: -> pushes a value into a binding, <- pulls a value into a hole. The carve can do either at any position.

This is genericity without a separate generic syntax.

A list can be described as a scope with a pulled element shape:

List -> {
  T <- none

  -> {}
  -> { T:, ...List{T}: }
}

The first production is the empty list. The second production is a head shaped like T followed by another List{T} expanded into the same structure. The recursive reference List{T} propagates the same hole — it does not refill it.

Use it:

List{T <- u8}:numbers

T <- u8 fills the hole at the use site. As with identity, T can also be left to inference when the carving carries enough shape to recover it.

Generic abstractions are just scopes with holes.

A serializer can be modeled the same way:

Serializer -> {
  S <- {}
  R <- {}

  encode -> {
    S:value
    -> R:
  }

  decode -> {
    R:value
    -> S:
  }
}

Eventually, laws can be added to the same scope:

Serializer -> {
  S <- {}
  R <- {}

  encode -> {
    S:value
    -> R:
  }

  decode -> {
    R:value
    -> S:
  }

  roundTrip <- {
    S:value -> ??
    -> decode{value -> encode{value -> value}!}! = value ?! true
  }
}

That is not only an interface. It is an algebraic contract: operations plus obligations.

Proof obligations are long-term. The generic structure does not depend on them.


Effects as nominal events

Syntact is structural by default. Effects are the exception: they are nominal because sometimes structural equality is not meaning equality.

Two events may have the same payload and still be different capabilities. A Log and an Audit event can carry the same string and still mean very different things. The structure cannot tell them apart; only the name can.

Nominality is not a property of ordinary data in Syntact. It is introduced explicitly through effects.

Values are structural. Shapes are structural. Patterns are structural. Modules are structural. Scopes are structural.

Effects are different. Effects are nominal events with structural payloads.

Log -> {
  String:message
}

Audit -> {
  String:message
}

Log and Audit have the same structure, but they do not mean the same thing. A Log handler must not accidentally handle an Audit event.

So the rule is:

internal computation is structural
effects are nominal capabilities

Emit an event with >-:

>- Log{message -> "hello"}

Handle an event with -<:

Log -< e {
  -> io.write{e.message}!
}

A full example:

program -> {
  Log -< e {
    -> io.write{e.message}!
  }

  >- Log{message -> "hello"}
  -> 0
}

-> program!

Handlers are scoped. The first visible handler handles the event. After handling, execution resumes at the point where the event was emitted.

This is Syntact's version of algebraic effects. They are called events because they are emitted and handled, but they are not callbacks, observers, or pub/sub messages.


The external boundary

Pure Syntact reduces toward singletons. But a real program eventually has to talk to something it cannot reduce: the kernel, a linked library, the hardware. That is the external boundary, and it is not a special feature — it is just a scope whose production points outside.

kernel -> <kernel.so>{
  write -> {
    u8:a  u8:b
    -> ??::u8
  }
  read -> {
    i32:fd  usize:len
    -> ??::isize
  }
}

<kernel.so> is provenance: it tells the compiler where the scope's leaves come from, and maps directly to one import descriptor. Everything inside is an ordinary scope. write is a scope with colored input bindings (u8:a, u8:b) and a production -> ??::u8.

That production is the key. ?? is an unknown value; ::u8 forces it into the u8 layout. So ??::u8 reads as "a value that is not computable in pure Syntact, but whose layout is known to be u8". The body is structurally empty — only the shape of the result is known, not the result. That is exactly what makes a leaf external.

Calling an external is ordinary scope algebra

Because write is just a scope, there is no special call syntax. Carving and collapse do the work, the same as everywhere else:

kernel.write              // projection — the scope, not executed
kernel.write{2, 3}!       // positional carve (a <- 2, b <- 3), then collapse
kernel.write{a -> 2 b -> 6}! // nominal carve, then collapse

partial -> kernel.write{b -> 4}  // partial carve, NO collapse — pure data, no effect
partial!                         // collapse here → the effect happens here, only now

Carving an external does not execute it. A partially-applied external is just another scope — pure data. The effect happens at !, and only there. This is consistent with the rest of the language: effects live at collapse points.

The effect marker is the frontier, not the result

An external collapse is effectful because the target is an external leaf, not because its production fails to reduce to a point. This matters:

  • A void/no-return external (e.g. closing a handle for its side effect) still performs an effect, even though its result folds to none.
  • An external returning a constant still performs an effect — the act of crossing the boundary is the effect, not the shape of what comes back.

So the rule is: an effect is lifted whenever a collapse crosses the external frontier, regardless of whether the production is singleton, non-singleton, or void.

No glue

This is where the one-world model pays off. In a language with a boxed runtime, calling a C library means writing a translation layer — unwrapping objects, marshalling, refcounting — for every binding, maintained by hand. That glue exists because there are two representations that do not speak to each other.

Syntact has one representation. A String, an array, a scope are values in the machine layout, not boxed objects — there is no pointer type in the pure language; the pointer only appears in boundary codegen, derived mechanically by a size rule (a value larger than a register is passed by address, otherwise by value). So there is nothing to translate. You declare the provenance, color the signatures, and the library is a scope you carve and collapse like any other.

You can even prove safety at the frontier. A C string is "any non-null char, then a terminator", which is a content constraint:

CString -> (~'\0').. + '\0'

A String satisfying CString is statically known to be a well-formed C string — no interior null — before it ever crosses the boundary.

Writing a library in Syntact

The same shape works in reverse. An external library is a scope whose production points out; a library written in Syntact is a scope whose production reduces in. They are the same object, seen from two sides — there is no separate notion of "a library".

So you do not need to drop into C for the fast path. A Syntact library is structure that folds: when its inputs are known it reduces to a singleton at compile time, and when they are not it reduces to its op-minimal symbolic form. It reaches codegen already optimized by construction, it is inspectable instead of being an opaque blob, it specializes at the call site through carving, and it cross-compiles by an arch flag instead of shipping one binary per platform. There is nothing to bundle.

The external boundary is therefore the exception — reserved for code you do not control (the kernel, a proprietary .so). Everything else is written in Syntact: pure, reducible, optimized by reduction.

Note: the external boundary is design, not yet implemented. The <lib>{} provenance form, :: raw casts, and the ?? unknown describe where the language is going; the cast and the unknown already fold in the bootstrap compiler, the <lib>{} boundary does not parse yet.


Handlers as compile-time dependency injection

Handlers make many runtime dependency injection patterns unnecessary.

In a classical language, if code needs an allocator, logger, clock, database, random source, HTTP client, or filesystem, you often pass a value around:

function(..., allocator, logger, db, clock)

or you hide it behind an object, interface, global, context, or DI container.

In Syntact, the code emits a nominal event. The surrounding scope decides how to interpret it.

Alloc -> {
  usize:size
}

Buffer -> {
  usize:size
  ptr -> >- Alloc{size -> size}
  -> ptr
}

One scope may choose malloc:

WithMalloc -> {
  Alloc -< e {
    -> malloc{e.size}!
  }

  -> Buffer{size -> 1024}!
}

Another may choose an arena:

WithArena -> {
  Alloc -< e {
    -> arena.alloc{e.size}!
  }

  -> Buffer{size -> 1024}!
}

Buffer does not receive an allocator. There is no allocator variable. There is only a nominal effect resolved by the current scope.

A library can be specialized by carving its handler:

FastLib -> SomeLib{
  Alloc -< e {
    -> arena.alloc{e.size}!
  }
}

This is dependency injection moved from runtime to compile time.

It is also an optimization surface. If the handler is known at collapse time, an allocation event can become a malloc call, an arena bump, a stack allocation, a pooled allocation, or disappear entirely if the reduction proves it unnecessary.

The same idea applies to:

logging
profiling
database access
transactions
filesystem permissions
randomness
time
HTTP clients
test mocks
sandboxing
error policy

In other languages, this often requires DI, interfaces, mocks, macros, build-time configuration, or runtime lookup. In Syntact, it is scope and handler selection.


Resonance

Resonance is the explicit model for state.

The idea:

mutation = value driven by nominal event

A resonant binding uses >>- and -<<.

Counter -> {
  Change -> { u8:value }

  -> {
    u8:value >>- Change -> 0

    Change -< e {
      value -<< e.value
    }

    increment -> {
      >- Change{value -> value + 1}
    }

    decrement -> {
      >- Change{value -> value - 1}
    }

    -> value
  }
}

>>- declares that a binding is resonant: it can change, but only through a named event. -<< performs the actual update inside the handler.

There is no hidden mutable field. The state changes only through a visible nominal event.

A reusable state abstraction can be a normal scope:

State -> {
  T <- none
  T:initial

  -> {
    Update -> { T:value }

    T:value >>- Update -> initial

    Update -< e {
      value -<< e.value
    }

    set -> {
      T:value
      >- Update{value -> value}
    }

    -> {
      -> value
      set -> set
    }
  }!
}

Resonance is not part of the first implementation. Events come first. Resonance is built on top of events.


Reactivity

Reactivity is the implicit model for derived state.

Where resonance requires an explicit event to drive change, a reactive binding automatically recomputes when its dependencies change. The operators are >>= and =<<.

Reactive bindings with >>=

>>= declares a binding whose value is derived from an expression and recomputes when that expression's dependencies change.

Counter:globalCounter

bool:counterPositive >>= globalCounter.value >= 0

counterPositive is not set once. It tracks globalCounter.value and recomputes whenever it changes. If globalCounter is driven by resonance, then counterPositive reacts to each resonant update without needing its own event.

A reactive binding can also be combined with resonance on the same binding:

T:value >>- Update =<< initial

This means: value is resonant (driven by the Update event) and initially bound by reference to initial. The >>=/=<< side provides the initialization and structural link; the >>- side provides the mutation channel.

Reactive productions with =<<

=<< without a left side declares a reactive production: a side effect that re-executes when its dependencies change.

Text -> {
  String:text =<< ""
  =<< text ? {
    -> >- Redraw{}
  }
}

When text changes, the production re-evaluates and emits a Redraw event. This is how a UI component can react to its own state without polling or manual subscriptions.

Resonance vs reactivity

The two mechanisms serve different roles and compose together:

resonance   explicit state change through a nominal event
reactivity  implicit derived computation that tracks dependencies

Resonance is where mutation happens. Reactivity is where propagation happens. A reactive binding can observe resonant bindings, other reactive bindings, or any binding whose value may change.

State -> {
  T <- none
  T:initial
  -> {
    Update -> { T:value }
    T:value >>- Update =<< initial
    Update -< e { value -<< e.value }
    update -> { T:value, >- Update{value} }
    -> { -> value, set -> update }
  }!
}

Then UI state can be built by libraries, not special syntax:

CounterView -> {
  State{initial -> 0}:value

  -> Column{
    children -> {
      Text{content -> value!}

      Button{
        label -> "Increment"
        onClick -> {
          value.set{value -> value! + 1}!
        }
      }
    }
  }
}

State, Column, Text, and Button are scopes. The SDK should be a library of scopes, not a second language.

Neither resonance nor reactivity is part of the first implementation. Events come first. Resonance is built on top of events. Reactivity is built on top of resonance.


Files, folders, and imports

Files and folders are scopes.

@ resolves the filesystem as a scope graph.

Plane2D -> @lib.geometry.Plane

A folder is a scope whose bindings are its files and subfolders. A file is a scope whose bindings are its top-level declarations.

Importing is expansion:

...@lib.geometry

A library can be carved before expansion:

...@lib.geometry{
  Plane -> Plane{dimension -> 3}
}

A handler can be overridden the same way:

FastGeometry -> @lib.geometry{
  Alloc -< e {
    -> arena.alloc{e.size}!
  }
}

There is no separate import ontology. The filesystem is a scope graph, and imports are scope operations.


Compile-time and metaprogramming

Syntact blurs the line between programming and metaprogramming because a program before collapse is already data.

In other languages, manipulating a class as data requires reflection, annotations, code generation, templates, macros, or compiler plugins.

In Syntact, the “class” is a scope. You can carve it, inspect it, constrain with it, expand it, or collapse it with the same operators used everywhere else.

Many things that are metaprogramming elsewhere become ordinary programming:

constructor generation  -> defaults + carving
copyWith                -> carving
schema derivation       -> scope inspection
generic specialization  -> pull binding + carving
macro expansion         -> scope transformation
DI configuration        -> handler override
mocking                 -> local handler override
compile-time constants  -> pure collapse
module specialization   -> carved expansion

A pure computation can be reduced by the compiler:

greeting -> "hello, " + "world"
-> greeting

No runtime concatenation is necessary.

Effects mark the boundary. If collapse reaches an event that must happen at runtime, that work remains runtime. If the event has a compile-time interpretation, it can be reduced earlier.

The compiler and runtime are not different semantic engines. The compiler is the reducer used before runtime.


Proofs

Proofs are long-term, not part of the first usable version.

The intended operators are:

??  symbolic unknown
?!  proof obligation

Example:

decodeEncodeSymmetry -> {
  String:m -> ??
  -> decode{value -> encode{value -> m}!}! = m ?! true
}

Or as a law inside a scope:

Serializer -> {
  S <- {}
  R <- {}

  encode -> {
    S:value
    -> R:
  }

  decode -> {
    R:value
    -> S:
  }

  roundTrip <- {
    S:value -> ??
    -> decode{value -> encode{value -> value}!}! = value ?! true
  }
}

The point is not to attach a separate proof assistant to the language. The point is to ask the same reducer a stronger question: can this property be proven for every value of this shape?

This must be added carefully. Proofs can make compile time explode. The first versions should not depend on them.


Why this should be fast

Traditional languages create abstraction barriers, then optimizers try to remove them.

A function call hides a body. A method hides a function behind a receiver. A trait or interface hides an implementation. A closure hides capture. A dependency hides behind a parameter. A framework hides control flow.

Syntact exposes more structure directly.

When you write:

square{n -> 5}!

you are asking the compiler to reduce the scope square under a known carved binding.

When you write:

WithArena -> {
  Alloc -< e {
    -> arena.alloc{e.size}!
  }

  -> parse!
}

you are asking the compiler to reduce parse under a known interpretation of Alloc.

The compiler sees:

bindings
defaults
carvings
productions
constraints
handlers
collapse points

It does not need to rediscover all of that through a maze of functions, objects, interfaces, and runtime configuration.

The collapse operator is therefore not just execution syntax. It is an optimization request:

reduce everything that can be reduced, and keep only what must remain.

The ambition is to write extremely high abstractions and pay only for the machine work that survives reduction.

This is not just an aspiration — it is what the bootstrap compiler already does. A program that stacks dozens of multiplications, distributions, cancellations, and telescoping sums over three runtime arguments:

a -> ??::u8 ; b -> ??::u8 ; c -> ??::u8
t1 -> (a*7 + 3)*5            // and many more layers…
u1 -> 2 * (t1 - 5*a)
v1 -> u1 + a*9 - a*9 + 100 - 100
// …seventeen lines of compounding arithmetic…
-> big*2 - (big + 7) + 8

reduces to its minimal affine form 60·a + 78·b + 40·c, and the x64 backend emits the arithmetic core a production C compiler at -O3 would — all 32-bit, every multiply by a constant folded into imul/lea, the additions fused into address-mode lea, no spills, no wasted moves. The abstractions cost nothing; only the surviving computation is paid for.

Benchmarked against the exact C equivalent (return 60*a + 78*b + 40*c;) on the same inputs:

Syntact gcc -O3 clang -O3
arithmetic core imul+lea, 8 insns equivalent equivalent
binary size 472 B 15 976 B 15 984 B
process startup (hyperfine) 152 µs 450 µs 462 µs
compile time — to a runnable executable (hyperfine -N) 5.3 ms 36.9 ms 52.1 ms
compile time — front-end + optimizer only (-c, object, not yet runnable) 24.3 ms 26.9 ms

The generated arithmetic is on par with -O3 — gcc/clang do not beat the LLVM-style instruction selector. Syntact's edge is structural: no ABI, no libc, a minimal static _start that parses argv inline and exits by syscall. So the binary is ~34× smaller and starts ~3× faster. (The startup gap is dominated by libc init and strtol@plt calls, which Syntact has neither of; a heavy compute loop would close it, since the arithmetic itself is equivalent.)

On compile time Syntact produces a runnable ELF in ~5.3 ms — ~7× faster than gcc and ~10× faster than clang to their final executables. The fair reading is structural, not a smarter optimizer:

  • Linking is a large slice of the gcc/clang number, not parsing. Stopping at -c (object file, no link) drops gcc to 24.3 ms and clang to 26.9 ms — so the link step alone is ~12.6 ms for gcc and ~25.2 ms for clang (about half of clang's total). The front end is noise in both chains: C is not "bigger to parse" than Syntact. Syntact has no separate link step, no libc, no crt — its bytecode lowers straight to a monolithic static ELF.
  • Even removing the link entirely, gcc/clang stay ~4.6–5.1× slower (24–27 ms for an object that still needs linking, vs Syntact's 5.3 ms for a finished executable). That residual gap is their general-purpose machinery — a heavyweight IR (GIMPLE/RTL, LLVM IR) and optimization passes that run in full on even a trivial program, including overflow-absence proofs and general dataflow analysis. Syntact's reducer knows every value's range by construction, so there is no overflow proof to do, and there is no general IR between bytecode and ELF.

So the compile-time win is the same architectural fact as the size and startup wins — no libc/link, range known by construction — not a cleverer optimizer.


A small practical comparison

A server config in a classical language often needs a class, constructor defaults, validation, and a copy method.

In Syntact:

Port -> u16 & >0

ServerConfig -> {
  String:host -> "localhost"
  Port:port -> 8080
  bool:debug -> false
}

ServerConfig:config{port -> 3000}

prod -> config{
  host -> "0.0.0.0"
  debug -> false
}

No constructor. No builder. No copyWith. No nullable parameters. The shape and carving algebra do the work.

An endpoint should not need endpoint-specific syntax. It should be a scope shaped by a library scope.

RestEndPoint:userEndpoint{
  path -> "/users/:id"

  get -> {
    maybeId -> Maybe{value -> req.path.get{"id"}!}!

    -> maybeId ? {
      {}: -> HttpResponse{
        status -> 400
        message -> "Invalid id"
      }

      UserId:(id) -> {
        user -> db.users.find{id -> id}!

        -> user ? {
          none -> HttpResponse{
            status -> 404
            message -> "User not found"
          }

          User:{id name} -> HttpResponse{
            status -> 200
            message -> Json.encode{value -> user}!
          }
        }
      }
    }
  }
}

RestEndPoint, HttpResponse, UserId, Maybe, and Json are scopes. The SDK should provide powerful scopes, not ad-hoc syntax.


What Syntact gives up

Syntact gives up:

function as primitive
class as primitive
struct as primitive
module as primitive
mutation as primitive
runtime DI as primitive
macros as a separate language
imports as a separate system
type/value split as a hard boundary

In exchange, it tries to get:

one world of data
complete scopes by default
structural derivation
explicit reduction
structural shapes
first-class patterns
nominal effects
scoped handlers
compile-time dependency injection
metaprogramming without a meta layer
resonance for explicit state
reactivity for derived bindings
proofs as future reduction obligations

The promise is not that everything becomes easy. The promise is that the hard things belong to one algebra instead of ten incompatible subsystems.


Implementation plan

Syntact is too ambitious to build all at once.

The implementation grows in layers. Each layer must be useful by itself. The language is still in its initial development cycle, so the milestones are numbered under a single v0 line — v0 is the executable core, v0.1v0.5 add each layer on top — rather than as separate major versions.

v0 — Core executable language

Goal: prove that scope + binding + carving + collapse works.

Include:

parser
scopes
bindings with ->
productions
access with .
carving with {...}
collapse with !
primitive values
basic static analysis
simple backend

Exclude:

events
resonance
full scope algebra
proofs
concurrency
advanced grammars
large SDK

This must work:

square -> {
  n -> 0
  -> n * n
}

-> square{n -> 5}!

Status: done, and past "simple backend." The bootstrap compiler runs parse → analyze → reduce → bytecode → native x86-64 ELF, with an optimizing backend (linear-scan + coalescing, LEA instruction selection, 32-bit-width arithmetic). Scopes, bindings, productions, access, carving, collapse, primitive values, and constraint analysis all work.

v0.1 — Shapes and patterns

Goal: make Syntact useful for small real programs.

Include:

:
primitive shapes
user-defined shapes
pattern matching with ?
structural destructuring
anonymous shaped bindings
basic refinements

This enables:

Circle -> {
  u8:radius
}

SmallCircle -> Circle{radius?<10}

area -> {
  SmallCircle:{radius(r)}
  -> r * r * 3
}

Status: mostly done. Constraint coloring (:), primitive and user-defined shapes, pattern matching with ? (typecheck and value branches, exhaustiveness), anonymous shaped bindings, set-algebra constraints (&/|/~), and ranges all work and compile to native code. Structural destructuring with capture (Circle:{radius(r)}) and full carve materialization are the remaining gaps.

v0.2 — Nominal events

Goal: introduce Syntact's algebraic effects.

Include:

nominal event declaration
event emission with >-
handlers with -<
lexical handler resolution
missing-handler errors
handler override through carving

This enables:

Log -> {
  String:message
}

program -> {
  Log -< e {
    -> io.write{e.message}!
  }

  >- Log{message -> "hello"}
  -> 0
}

v0.3 — Resonance and reactivity

Goal: model state, mutation, and derived bindings.

Include:

>>-    resonant binding declaration
-<<    resonant update inside handler
>>=    reactive derived binding
=<<    reactive production
resonant bindings driven by nominal events
reactive bindings that track dependencies
state abstractions as library scopes
UI-friendly reactive patterns

v0.4 — Fuller scope algebra

Goal: close the algebra.

Include progressively:

&
|
~
ranges
sequence grammars
shape refinement
exact vs derived shape relations
first-class reusable patterns
module/scope algebra

This is where Email, Identifier, SmallCircle, weirdInt, JSON grammars, and refined domain shapes become central.

v0.5 — Proofs

Goal: add compile-time obligations carefully.

Include only after the rest is stable:

??
?!
limited symbolic reduction
law checking
serializer round trips
simple algebraic properties

Proofs are powerful, but they are not required to make the language useful. They are the long-term destination.


Final note

Syntact is not trying to be a small syntax experiment.

It is an attempt to build a programming language from a different computational ontology: one world of complete scopes, manipulated algebraically, reduced explicitly.

If that idea feels strange at first, good. It should. The goal is not to decorate the old categories. The goal is to remove them.

Syntact is the language I wished existed. If, after reading this, you wish it existed too — you're in the right place.