LA3 Loading La³, please wait
Skip to content

Pillar 2 · the chosen answer to "embedded"

The À-la-carte Dynamic Standard Library

Also known as stdlib à la carte. La³ explicitly rejects a no_std split. Instead, the standard library is a set of many small, fully independent modules, and a build pulls in only what the program actually uses.

The goal, in one paragraph

One language for a microcontroller and a desktop app

The same front-end that type-checks a web app (exact-width integers, ownership, raw pointers, C-style layout) is exactly what bare metal needs. The real split is the runtime and the target, not the language.

So the standard library is not one monolith and not a no_std fork. It is a field of independent modules joined only through a thin capability layer. A granular build keeps just what main reaches and lets co-present modules share; a monolithic build takes the lot. Both behave identically.

The contract

Six requirements, R1 through R6

The design must satisfy each of these. They are not aspirations: they are the testable contract the mechanism is built to meet.

R1

Independence

A module used alone references nothing else. Each module ships a private fallback for every capability it needs, so it builds and works with no other module present.

R2

Usage-driven inclusion

The final artifact contains code for a module only if the program actually reaches it. Dead code is pruned at module and symbol granularity.

R3

Opportunistic sharing

If two modules are present and one could reuse what the other already brings, it may fold onto that implementation: sharing only ever removes duplication, never adds a dependency.

R4

Two modes

A build flag selects granular (independence + sharing + aggressive DCE, for the Pico and kernels) or monolithic (the whole stdlib, free to interdepend, the default for full apps).

R5

Behavioural identity

For any program, the granular and monolithic builds are observationally identical: same output, same semantics. Only size and layout differ.

R6

Determinism

Given the same source, module set and flags, resolution produces the same provider choices every time. Provider precedence makes every binding reproducible.

The module model

Modules declare a capability surface

Every module declares what it can provide to others and what it wants from them, and ships a private fallback for each want, so it never hard-depends on anyone. That fallback is what keeps R1 true.

text.la3
module text {
    // "I can provide utf8_decode to others (canonical)."
    @provides(utf8_decode v1.0.0 = text::decode)

    // "I need a growable buffer; here is my private fallback,
    //  used when no external provider is in the build."
    @wants(growable_buffer ^1)

    fn decode(raw: &[u8]) -> Result<str> { /* ... */ }
}

Capabilities

The sharing currency

A capability is a small interface declared once, centrally: a contract between modules, not inside any one of them. Sharing is sound because every implementation passes the same conformance suite, so one can be swapped for another with no observable change (R5).

capabilities/growable_buffer.la3
capability growable_buffer v1 {
    type Buf                          // opaque to wanters
    fn new() -> Buf
    fn push(b: &mut Buf, byte: u8)
    fn as_slice(b: &Buf) -> &[u8]
    fn len(b: &Buf) -> usize
}

The capability resolver

A least fixpoint, seeded from main

Resolution is not a single pass: binding a want pulls in a provider, whose code reaches new wants, which need binding too. So it grows the reachable symbol set and the bindings together until nothing changes.

Provider precedence makes every choice deterministic (R6), and a wanter’s own fallback is always a valid last resort: precisely why the alone build (R1) can never fail.

resolve.la3
// One resolver, two present-sets.
present =
    mode == granular
        ? reachable_from(main)
        : all_modules
reachable = symbols_from(main)

// Least fixpoint: grow bindings and reachability together.
repeat until neither bindings nor reachable changes {
    for each reachable wants(C, range) {
        candidates =
            providers in present matching (C, range)
        binding =
            select_by_precedence(candidates)
            ?? wanter.fallback
        reachable += symbols_of(binding)
    }
}

Two modes, one resolver

Same program, two present-sets

The build mode changes exactly one input to the resolver: which modules count as present. Everything else is identical, which is why the outputs behave identically (R5).

granular --stdlib granular
Present-set
only modules reachable from main
Effect
Fallbacks fill the gaps; co-present modules deduplicate via fallback-promotion. Out-of-line shared symbols and aggressive dead-code elimination.
Target
Raspberry Pi Pico · kernels · bare metal
monolithic default
Present-set
every stdlib module
Effect
The whole standard library is available and free to interdepend, tuned for throughput rather than footprint.
Target
Desktop apps · web · servers

Behavioural identity (R5) is the headline conformance test: a granular build and a monolithic build of the same program must produce the same output and the same semantics. Only size and layout may differ.

Vocabulary

Terms, used precisely

Module
The unit of independence, versioning and capability declaration: the smallest thing that can be present or absent in a build.
Capability
A small interface declared centrally: the contract between modules and the currency of all sharing.
Wanter
A module that needs a capability. It declares wants C and ships a private fallback implementation of it.
Provider
A module that offers an implementation of a capability for others: canonical (preferred) or a fallback promoted to serve others.
Present-set
The set of modules considered available during resolution. This single input is what distinguishes the two build modes.
Resolution
The whole-program pass that binds every wants C to exactly one provider (or the wanter’s own fallback), to a fixpoint.
Conformance suite
The executable contract of a capability: a battery every provider and fallback must pass. Sharing is sound because both sides pass the same suite.

Section 6.1 · worked example

A granular build, step by step

main uses only json. Watch the resolver grow the reachable set to a fixpoint and deduplicate growable_buffer onto a single promoted fallback.

The program

main.la3
use json;

fn main() {
    let raw = b"{\"hello\": 42}";
    let v   = json::parse(raw).unwrap();
    println!("{}", v);
}

json module

json.la3
module json {
    @wants(growable_buffer ^1)  // fallback: json::buf_fallback
    @wants(utf8_decode     ^1)  // fallback: json::utf8_fallback

    pub fn parse(raw: &[u8]) -> Result<Value> { /* ... */ }
}

text module

text.la3
module text {
    // canonical provider of utf8_decode
    @provides(utf8_decode v1.0.0 = text::decode)
    @wants(growable_buffer ^1)  // fallback: text::buf_fallback

    pub fn decode(raw: &[u8]) -> Result<str> { /* ... */ }
}

Resolution trace

  1. Step 0 Seed

    reachable = symbols_from(main) -> json::parse

  2. Step 1 Pull json

    json is reachable -> add its wants: growable_buffer ^1, utf8_decode ^1

  3. Step 2 Bind utf8_decode

    text is present (reachable via json) -> bind json's wants(utf8_decode) -> text::decode. Pull text into reachable.

  4. Step 3 text also wants growable_buffer

    Now text is reachable -> its wants(growable_buffer ^1) must be resolved too.

  5. Step 4 Promote fallback

    No canonical growable_buffer provider in present-set. json's fallback has higher priority (declared first). Bind both json and text onto json::buf_fallback.

  6. Step 5 Fixpoint

    Neither bindings nor reachable changed. Done. Artifact: main + json + text. growable_buffer served by json's promoted fallback.

Final artifact

main + json + text. No separate growable_buffer module; both wanters converge on json::buf_fallback. R1, R2, R3, and R6 all hold.

Section 5.2 · pipeline

Where Phase 12 sits in the compiler

Capability resolution runs after all type-level work is done: monomorphisation, MIR, optimisation. It sees concrete, fully specialised symbols and is a single whole-program pass with no back-edges into earlier phases.

After the fixpoint, Phase 13 rewrites every bound call site and runs link-time DCE. Phase 14 emits the final object, WASM, or LLVM IR.

  1. 1-4

    Lex, Parse, Desugar, Name res.

  2. 5

    Type inference

  3. 6

    Borrow check

  4. 7

    Monomorphisation

  5. 8-11

    MIR, Optimise, Lower, Validate

  6. 12

    Capability resolution <- here

    Seed from main; grow present-set; bind every reachable wants C to fixpoint.

  7. 13

    Link-time DCE + ABI rewrite

  8. 14

    Object / WASM / LLVM IR emit

No rush. Do it well.

The à-la-carte stdlib is Phase 12: a durable goal, not a deadline. The full design records the requirements, the resolver and its fixpoint, the ABI, worked examples and open questions.