Forward Track: Surface Design and Audience Reach

Forward-looking design document. Architectural commitments about how the language presents itself to different users — practitioners, researchers, library authors, systems engineers, production engineers, verification engineers, newcomers — without fragmenting into multiple languages or compromising on its technical foundation.

1. Framing

The question that triggered this document: can the language be designed to be fluid and friendly while reaching multiple audiences with genuinely different needs?

The short answer is yes, but it's the hardest design problem in the project. Harder than the type system, harder than the runtime, harder than verification. The reason: serving multiple audiences forces tradeoffs that the technical work doesn't, because the audiences have different and sometimes conflicting requirements. Types help library authors and verification engineers; they feel like friction to practitioners. Explicit control helps systems engineers; it hurts ergonomics for everyone else. Stability helps production but constrains research.

This document commits to a strategy: one surface language with progressive disclosure, persona-aware defaults, and bidirectional inference, supported by multi-tier documentation and migration tooling. The bet is that the project's type-system foundation gives us more capacity to serve multiple audiences than a typeless language has, because the types are doing work even when invisible.

If the bet is right, this is a real differentiator — most ML language projects pick one audience and hope others adapt. If it's wrong, the surface ends up complicated and frustrates everyone. Phase 7 is where the strategy gets tested.

2. The audiences

Seven distinct user groups. The needs are real; the tensions are real.

2.1 ML practitioners

The largest group by volume. Currently use PyTorch or JAX. Write models, train them, debug them. Don't think of themselves as language users — they think of themselves as model builders.

Want: PyTorch-like ergonomics. Concise syntax. Forgiving errors. Quick iteration. Familiar idioms.

Tolerate: Some learning curve if the payoff is clear (e.g., better debuggability).

Hate: Verbose type signatures. Explicit memory management. Anything that interrupts the model-building flow.

2.2 Researchers

Often the same people as practitioners, but in a different mode. Exploring new architectures, publishing papers, breaking conventions to test ideas.

Want: Maximum flexibility. Easy escape hatches. Reproducibility (pinned versions, deterministic behavior).

Tolerate: Rough edges in less-trodden paths.

Hate: Constraints that force them to fit ideas into existing categories.

2.3 Library authors

Building reusable abstractions on top of the runtime. Domain-specific libraries (typed dataframes per the Arrow track), application-specific extensions, internal company tools.

Want: ABI stability. Explicit types at module boundaries. Clear extension mechanisms. Documentation that's deep enough to build production code against.

Tolerate: Verbosity at boundaries; that's where types earn their keep.

Hate: Internal-only APIs they need but can't rely on. Frequent breaking changes. Documentation that assumes prior knowledge.

2.4 Compiler / systems engineers

Optimizing kernels, doing performance work, building infrastructure. Comfortable with explicit memory layouts, hardware capabilities, low-level control.

Want: Explicit control over lowering, memory, and execution. Predictable performance. Access to hardware features. Good profiling integration.

Tolerate: Verbose syntax when it buys explicit semantics.

Hate: Black-box magic. Implicit operations they can't trace through. Performance unpredictability.

2.5 Production engineers

Deploying ML systems at scale. Care about reliability, predictable performance, deployment story.

Want: Reproducibility. Stable ABIs. Clear deployment patterns. Good observability (per Phase 1 Section 4). Failure modes that are well-defined.

Tolerate: Some operational complexity if the payoff is reliability.

Hate: Surprises in production. Performance regressions. Anything that makes incident response harder.

2.6 Verification engineers

Proving properties of ML systems — correctness, security, robustness, sometimes safety. The smallest group by count, but the one whose needs the project's foundation is uniquely positioned to serve.

Want: Formal semantics. Mechanizable type system. Clear extensibility for verification annotations.

Tolerate: Almost any complexity if it serves provability.

Hate: Informal specifications. Implementation behavior that diverges from specified behavior. Anything that introduces unverifiable assumptions.

2.7 Newcomers

Students learning ML; engineers from adjacent fields; anyone encountering the language for the first time.

Want: Approachable concepts. Good error messages. Learn-by-doing tutorials. Help when stuck.

Tolerate: Complexity if it's introduced gradually.

Hate: Walls of jargon. Errors they can't decode. Examples that assume prior context.

3. The same-person-different-modes insight

The seven audiences look like seven separate user groups requiring seven separate solutions. They're not. The same person occupies different audiences at different times in their workflow:

• An ML practitioner exploring a new architecture is in researcher mode.
• The same person debugging a shape mismatch is in library author mode — they want to see types now.
• The same person publishing a paper wants reproducibility, switching to production mode.
• The same person optimizing a slow kernel is in systems engineer mode.
• The same person formalizing the model's properties for safety review is in verification mode.

This reframing is the design strategy's foundation. The language doesn't need to serve seven separate groups with seven separate tools. It needs to support mode-switching within one workflow — and crucially, graceful mode-switching, where moving between modes doesn't force a rewrite.

The implications:

• One surface language, not multiple.
• The same code can be read at multiple levels of detail.
• Adding rigor (types, refinements, verification) is additive, not disruptive.
• Removing rigor (working in research mode) is also additive, not disruptive.

The technical question for Phase 7: what surface design supports this gracefully?

4. Five design strategies

The strategies that compose into the answer.

4.1 Progressive disclosure within one surface

Simple cases look simple. Complex cases require more explicit syntax. Same language; layers of detail revealed as needed. Swift and TypeScript exemplify this.

Concretely, three views of the same function:

Practitioner mode — types fully inferred:

def attention(q, k, v):
    return softmax(q @ k.T / sqrt(q.shape[-1])) @ v

Library-author mode — explicit at boundaries:

fn attention[B, H, S, D](
    q: Tensor[F32, [B, H, S, D]],
    k: Tensor[F32, [B, H, S, D]],
    v: Tensor[F32, [B, H, S, D]],
) -> Tensor[F32, [B, H, S, D]]:
    return softmax(q @ k.T / sqrt(D), axis=-1) @ v

Verification mode — refinements and proofs:

@verified(soundness = "structural")
fn attention[B, H, S, D]
    requires (D mod 8 == 0)
    requires (B > 0 and H > 0 and S > 0)
    (q: Tensor[F32, [B, H, S, D]],
     k: Tensor[F32, [B, H, S, D]],
     v: Tensor[F32, [B, H, S, D]],
    ) -> Tensor[F32, [B, H, S, D]]:
    ...

The three are the same language. The type system is always there. It's just not always visible. The surface allows progressive specification: write less, get inference; write more, get precision.

4.2 Bidirectional inference making types optional

Phase 0's bidirectional discipline (Section 3 §7 of Phase 0; Section 2 §5.2 of Phase 1) is exactly the right machinery. Inference fills in what the user omits; checking verifies what the user writes.

Without bidirectional inference, the user has to write everything:

let q_dim : Int = 64
let q : Tensor[F32, [4, 8, 256, 64]] = randn(...)
let scores : Tensor[F32, [4, 8, 256, 256]] = matmul q (transpose k -1 -2)
let attn : Tensor[F32, [4, 8, 256, 256]] = softmax scores 3
let out : Tensor[F32, [4, 8, 256, 64]] = matmul attn v

With bidirectional inference, the user writes intent; types follow:

let q_dim = 64
let q = randn (4, 8, 256, q_dim)
let scores = q @ k.T
let attn = softmax scores ~axis:(-1)
let out = attn @ v

The types still exist. The compiler can show them on demand (an LSP hover request returns the inferred type). Errors still surface them ("scores was inferred as Tensor[F32, [4, 8, 256, 256]]; expected Tensor[F32, [4, 8, 64, 64]]"). The user just didn't have to write them.

This is what makes the "fluid" surface possible without sacrificing the type system.

4.3 Persona-aware defaults via pragmas

A file-level (or block-level) pragma sets the rigor:

#![pragma(mode = "research")]
# types optional everywhere; warnings minimal; experimental features enabled

#![pragma(mode = "library")]
# types required at function boundaries; warnings as errors; ABI checks active

#![pragma(mode = "production")]
# library mode + reproducibility checks + deployment-quality diagnostics

#![pragma(mode = "verified")]
# library mode + verification obligations active + soundness checks

Same syntax; different defaults. Same compiler; different stringency. A practitioner's notebook is research mode (cuts ceremony). A library's lib.ai is library mode (enforces ABI discipline). Production code is production mode (catches issues that would burn during deployment).

The pragma approach is light-touch — most practitioners never set one explicitly; the default for an interactive REPL is research and the default for a published library is library. The pragma exists to override defaults, not to require ceremony.

4.4 Migration paths from existing tools

The single biggest barrier to adoption isn't the language; it's the cost of moving an existing codebase. Three commitments make this tractable:

Translation tools. A pytorch2ours translator that handles the common patterns:

• nn.Linear(in, out) → linear(in, out)
• F.relu → relu
• q @ k.transpose(-1, -2) → q @ k.T
• torch.softmax(x, dim=-1) → softmax(x, axis=-1)
• Most of nn.Module's surface area mechanically translatable

The output isn't perfect — some patterns need manual review — but for typical model code, the translator handles 80%+ of surface, leaving only the genuinely interesting parts for human attention.

Side-by-side documentation. Every common PyTorch / JAX pattern gets a translation showing how it looks in our language:

Familiar idioms preserved. Where PyTorch / JAX have established idioms that work — vmap, pmap, the @functools.partial patterns — our language preserves them. Where they don't work (PyTorch's training-mode flag pattern, dynamic-shape tracing) we replace them deliberately.

The cost is real engineering work: the translator alone is plausibly ~5K LOC of OCaml or Python; the documentation is ongoing maintenance. The benefit is enormous: practitioners can move existing code rather than rewriting from scratch.

4.5 Multi-tier documentation

Documentation organized by persona, not by feature.

ADRs live in decisions/ at repo root (Phase 0 Section 5), not under docs/.

docs/
├── tutorials/
│   ├── practitioner/        — "Building your first model"
│   ├── researcher/          — "Implementing a new attention variant"
│   ├── library-author/      — "Building a custom layer"
│   ├── systems-engineer/    — "Writing a custom kernel"
│   ├── production/          — "Deploying to production"
│   └── verification/        — "Proving a property"
├── reference/               — generated API docs (rustdoc-style)
├── architecture/            — internals; for contributors
├── migrations/
│   ├── from-pytorch/        — side-by-side translations
│   └── from-jax/            — same
└── papers/                  — formal results; for researchers

Each tutorial track is a complete entry point. A practitioner who lands on /docs/tutorials/practitioner/ doesn't need to read library-author content. A library author who lands on their tutorial doesn't need to read practitioner content. Same language; different framings of how to engage with it.

The reference docs (auto-generated) serve everyone but are a poor first read. The architecture docs serve contributors. The papers serve verification-engineers and researchers.

The cost is real: per-persona content is more total content than single-track docs. The benefit is that users find their entry point quickly and don't have to wade through irrelevant material.

5. Phase 7 commitments

The surface-syntax design phase is where these strategies become concrete language features.

5.1 Three Phase 7 hard commitments

1. One surface language, not multiple. Different surfaces for different audiences fragment the ecosystem. If a researcher writes code in "research surface" and a library author rewrites it in "library surface," the work doesn't compose. One language; modes shift the rigor, not the syntax.

2. Progressive disclosure as the design discipline. Every language feature must work at every disclosure level. Adding a type annotation must be additive (not require restructuring); removing one must be additive (not require code changes elsewhere). This is a constraint on every Phase 7 syntax decision.

3. Pragma-driven mode switching. File-level and block-level pragmas set rigor. Defaults are persona-aware (interactive REPL → research mode; lib.ai → library mode). Modes affect what's required, not what's allowed. A library-mode file can contain research-mode-style code; the compiler will warn rather than reject.

5.2 Phase 7 surface syntax requirements

What the surface needs to support:

• Function definitions at multiple disclosure levels. Inferred-type functions, explicit-type functions, refinement-typed functions, verified functions. All in the same syntax.
• Type annotations as opt-in. Never required at let-bindings inside function bodies. Required at function boundaries only in library / production / verified modes.
• Refinement annotations as opt-in. The requires clauses are optional; their absence means inferred refinements (or none).
• Decorator syntax for attributes. @verified, @no_gradient, @inline, @kernel. Decorators read like Python's; they activate compiler features.
• Pragmas at file and block level. #![pragma(...)] at file top; #[pragma(...)] on declarations.
• Module / namespace system. Standard ML or Rust-style; supports the library-author persona.
• Operator overloading for tensors. @, +, *, / work as expected. Same as PyTorch / NumPy / JAX.
• Indexing and slicing. x[..., :8] works as expected. NumPy-compatible indexing semantics.

5.3 Phase 7 surface syntax non-goals

Things Phase 7 should not try to do:

• Match PyTorch syntactically pixel-for-pixel. Differences are inevitable; pretending otherwise creates surprise. Document the differences clearly.
• Be Pythonic across the board. Pythonic where it's natural (function definitions, decorators, operator overloading); ML-flavored where it's better (algebraic data types, pattern matching, type annotations). Hybrid is fine.
• Allow arbitrary user-defined operators. Operator overloading is in scope; defining <*> for some custom semantics is not. Keeps code readable.
• Macros. Compile-time metaprogramming via macros leads to ecosystem fragmentation. Decorators handle the common cases; the bootstrap-and-self-modeling track's effect handlers handle the rest.

6. Phase 1 commitments

The cheap-now, expensive-later items that keep Phase 7's path open.

6.1 Library author's guide establishes persona discipline

The library author's guide v0.1 (Phase 1 Section 7 §9) is library-author-mode content. The guide should:

• Show all examples in library-author mode (explicit types, ABI annotations).
• Have a separate "research-mode tutorial" showing the same examples with inferred types.
• Note explicitly which surfaces are stable (the library-author concern) and which aren't.

This sets the precedent: the documentation acknowledges multiple personas from day one, even though only library-author mode is fully usable in Phase 1 (no surface syntax yet).

6.2 Error messages show inferred types

Phase 1 Section 2 §10 commits to good error messages with source locations and SMT counterexamples. Extend that commitment: error messages must show inferred types at the point of error.

Example:

error: shape mismatch in matmul
  --> example.ai:7:11
   |
 7 |   let scores = q @ k.T
   |                ^^^^^^^
   |
   = note: q has inferred type Tensor[F32, [4, 8, 256, 64]]
   = note: k.T has inferred type Tensor[F32, [4, 8, 64, 256]]
   = expected: Tensor[F32, [4, 8, 256, X]] where X matches q's last dim
   = found: Tensor[F32, [4, 8, 64, 256]]
   = help: did you transpose the wrong axes?

Even when the user didn't write types, the error shows what the compiler inferred. This is how practitioners learn the type system without being forced to write it. Commitment for Phase 1; investment pays off when Phase 7's research-mode lands.

6.3 Documentation organized by persona from day one

The Phase 1 documentation (Section 7 §10) defaults to per-persona organization:

• docs/tutorials/library-author/ — Phase 1's primary persona; the worked example lives here.
• docs/tutorials/practitioner/ — placeholder; full content arrives with Phase 7 surface syntax.
• docs/tutorials/systems-engineer/ — placeholder; Phase 5 fills in the kernel-authoring track.
• docs/tutorials/verification/ — placeholder; Phase 6 fills in the proof tutorials.

Each has a stub README explaining when its content lands. The structure is in place from Phase 1; the content arrives with the relevant phase.

6.4 Migration content for PyTorch patterns

A side-by-side document docs/migrations/from-pytorch.md lists every Phase 0/1 operation and its PyTorch equivalent. Initially small (only the operations Phase 1 implements); grows with each phase.

The full pytorch2ours translator is Phase 7+ work (it depends on the surface syntax existing). But the documentation pattern starts now.

6.5 The four commitments cost

These are small additions to Phase 1:

Within Phase 1's existing budgets (compiler 15K LoC, runtime 8K LoC, doc-build pipeline). No timeline impact; meaningful design impact.

7. The honest constraint

Designing for seven audiences is more expensive than designing for one. The costs:

• Documentation effort. Per-persona content is more total content. Tutorials for all six audiences eventually plus reference docs eventually plus migration content compound.
• Tooling effort. LSP support for incremental disclosure is real engineering work. Translation tools are ongoing maintenance. Each persona's tools want to be first-class.
• Language design effort. The surface syntax has to support the disclosure pattern at every feature. Adding a feature that doesn't disclosure-cleanly is harder; some otherwise-attractive features get rejected on disclosure grounds.
• Cognitive load on contributors. Every language design decision requires asking "which personas does this affect?" Some personas conflict; tradeoffs have to be made deliberately.

The alternative — designing for one audience and letting the others adapt — is what most language projects do. PyTorch designed for practitioners; researchers adapted; production engineers built deployment tooling on top; library authors fought against the dynamic nature; verification engineers mostly gave up. JAX similarly: designed for researchers; practitioners follow; production engineers struggle; verification engineers wait.

The bet for this project: the type-system foundation gives us more capacity to serve multiple audiences than a typeless language has, because the types are doing work even when invisible. Hidden but present types catch errors for practitioners; visible types document interfaces for library authors; SMT-checked refinements satisfy verification engineers; explicit refinements optimize for systems engineers. Same machinery, different views.

If the bet is right, this is a real differentiator. If it's wrong — if the surface gets too complicated trying to be all things to all people, or if the disclosure pattern doesn't hold up under real use — the project ends up with a language that's pretty good for one audience and frustrating for the rest. That outcome is recoverable (drop disclosure; pick the primary persona; focus) but it's a real risk.

The mitigating discipline: measure adoption per persona as the project progresses. If practitioners are using it but library authors aren't (or vice versa), that's signal that the surface is failing for one group. The metrics aren't precise but they're observable.

8. Connections to other forward tracks

The persona discipline unifies several other commitments:

• Bootstrap and self-modeling — handlers are the power-user surface for compiler engineers. The same handler that AD-as-effect uses is what a systems engineer would write to add a custom transformation. The library-author-and-power-user persona overlap is real; the handler mechanism serves both.

• Ecosystem architecture (library author's guide) — the library-author persona's primary interface. The library author's guide is the entry point for that persona; the runtime FFI is its instrument.

• Arrow + typed dataframes — domain extensibility for non-ML audiences. Typed dataframes serve a different audience (data engineers, observability folks, analysts) than the ML audiences this document focuses on. The same language, different libraries; different personas served by domain libraries built on the foundation.

• CUDA-native (tile IR) — the systems-engineer persona's surface. Phase 5's tile IR is a sub-language designed specifically for kernel-authoring; the systems-engineer persona engages with it directly.

These tracks aren't independent. They're four views of the project's commitment to multiple ways of engaging with one foundation. This document's persona-driven framing makes that commitment legible.

9. Open issues

1. LSP support is real engineering work. Hover shows inferred types; auto-complete suggests valid operations on a tensor based on its shape; jump-to-definition crosses module boundaries. A serious LSP implementation is plausibly ~10K LoC of OCaml; the project would need a contributor specifically on tooling. Phase 7+ work; flagged.

2. Pragma scope and inheritance. When a file pragma is library, what about an inner block that wants research? Block-level pragmas override file-level; nested overrides shadow outer; the obvious model. But corner cases (decorator-applied pragmas, conditional pragmas, the relationship to imports) need design. Phase 7 work.

3. The disclosure ceiling. Progressive disclosure works as long as moving up the rigor ladder doesn't require restructuring. There's a ceiling: at some point (verification mode with non-trivial proofs), structural changes are unavoidable. Where the ceiling sits and whether it's hit by typical workflows is empirically open until Phase 7 lands.

4. Migration tooling fidelity. A pytorch2ours translator that handles 80% of cases is good; one that handles 99% is much better but much more expensive. The translator's fidelity ceiling depends on PyTorch surface area not covered by our language. Some PyTorch idioms (dynamic shapes, training-mode toggles) don't translate; the tool produces best-effort output and flags hard cases.

5. Tutorial maintenance burden. Per-persona tutorials require ongoing updates as the language evolves. If contributors find the tutorial structure heavy, the tutorials rot. Mitigation: strict ownership (one maintainer per persona's tutorials), CI checks that tutorial code still compiles, contributor guidelines that flag tutorial impact.

6. Mode-switching pitfalls. A user copies code from a research-mode notebook into a library-mode file; suddenly type errors appear that weren't there before. Is this surprise or feature? The answer depends on framing: "your library-mode file caught issues your notebook missed" is feature; "your code stopped working" is surprise. Documentation has to set expectations clearly.

7. The "newcomer" persona is hardest. Practitioners have PyTorch experience; library authors have systems experience; verification engineers have formal-methods experience. Newcomers have no analogues to transfer from. Newcomer-track tutorials require more scaffolding than other tracks; cost is higher per page.

10. Summary

Five strategies that compose:

Three Phase 7 commitments:

1. One surface language, not multiple.
2. Progressive disclosure as the design discipline.
3. Pragma-driven mode switching.

Four cheap Phase 1 commitments:

1. Library author's guide acknowledges multiple personas.
2. Error messages show inferred types.
3. Documentation organized by persona from day one.
4. Migration content for Phase 1's operation set.

The bet: the project's type-system foundation gives us more capacity to serve multiple audiences than a typeless language has, because the types are doing work even when invisible.

The track unifies the other forward tracks. Bootstrap-and-self-modeling serves the power-user persona via handlers; ecosystem-architecture serves the library-author persona via the runtime FFI; CUDA-native serves the systems-engineer persona via the tile IR; Arrow + typed dataframes serves data-engineering personas via domain extensibility. This document names the unifying pattern: multiple ways of engaging with one foundation, each tuned to a particular kind of user, none requiring a separate language.

If the project ever does what it's designed to do, this track is what makes it accessible to more than one kind of user. Same language, multiple audiences, no fragmentation. That's the ambition.

End of surface design and audience reach forward track.