talk: Wasm Research Day 2026 — "Change the Tires, Not the Car" - #150
Merged
Conversation
A Zola section rendering slides through templates/talk.html — no slide framework, no CDN, self-hosted Atkinson faces, so the deck presents with the network unplugged. Nineteen slides across five acts, weighted to the factory (six slides) rather than the demo, per the "the pipeline is qualified once" framing the site already carries. Styles derive from the existing tokens in _variables.scss rather than a deck theme, so a slide looks like the site. Touch, because it is presented from an iPad: - swipe left/right, gated on the gesture being decisively horizontal (SWIPE_MIN 45px, 1.4x bias) so scrolling a long evidence block does not skip slides; disabled in overview, which is itself a scrolling grid - on-screen prev/next/overview/fullscreen at Apple's 44pt minimum target, quiet on pointer devices, always present on touch - touch-action: pan-y on slides so iOS does not claim horizontal swipes as back-navigation; manipulation on buttons to drop the double-tap zoom delay - 100dvh, since iOS Safari's 100vh hides the last line under the toolbars - safe-area insets so the chrome clears the home indicator - webkitRequestFullscreen fallback — iPad Safari has no unprefixed form - the hint line says "swipe to move" on a device with no hover One authoring trap worth recording: a blank line inside a raw-HTML block ends the block, so markdown resumed INSIDE a <pre> and turned a "# correctness:" log line into an <h1>. Evidence is now several <pre> blocks in a .stack rather than one with blank lines in it. Branch only. Not for merge or deploy before the talk. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…slot Overview was unusable on a tablet. Diagnosed rather than guessed: at 1180px every one of the thumbnails overflowed its clipped box by up to 2x and got cut mid-line, which is what "overlapping" looked like. Hand-shrinking each element type was never going to hold as slides were added. Thumbnails are now title cards — act label, heading, number, everything else suppressed — which cannot spill, stay legible at any width, and are more useful mid-talk anyway. Verified at iPad landscape: 0 spilled, 0 overlapping pairs, no slide needs scrolling, no evidence block overflows horizontally. The pipeline slide answered "what are the stages" but not "what goes in and what comes out", which is what the tool sites do well. Rebuilt as a flow with both sides named per stage, down to `ld` taking the .o plus three native functions and emitting firmware with no engine in it. Added the code that was missing, all of it lifted from the repo rather than written to look plausible: the real mmio interface and wdg-driver world, the actual compose/fuse/optimize/compile commands, the wdg contract that offers no stop next to the Kani property that proves no escape from Running, and shim-mmio.js beside the silicon read32 so the substitution is on one slide. Calibrated against the published schedule for the event: - the slot is 25+5, not 30 — merged two overlapping slide pairs, 23 -> 21 - the title is already published; the deck now uses it verbatim - added an opening slide crediting the four adjacent talks (one of them two hours earlier the same day) so the work positions against them instead of appearing to ignore them - moved the verification-scope slide out of the closing act into the factory act: it and "no runtime resident" are the two claims this venue has not heard, and both now land before minute 20 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
Measured rather than eyeballed. At iPad landscape (1180x820) the deck was rendering body text at 16.8px and CODE BLOCKS AT 11.6px. That is document sizing on a slide, and unreadable over a shared screen — which for a remote talk gets downscaled again on the way to the audience. The cause was mine: every clamp()'s MAXIMUM was set at web-body values (1.4rem body, .95rem code), so the text could never grow past ~22px/~15px no matter how large the display. Raised all fourteen steps of the scale. before -> after, at 1180x820 h1 46 -> 52 lead 20 -> 29 body 17 -> 25 ledger 14 -> 18 code 12 -> 18 flow 12 -> 16 Also fixes a specificity bug the measurement exposed: `.slide p` (0,2,0) beat `.slide__act` and `.slide__cite` (0,1,0), so the act eyebrow and every citation line had been rendering at FULL BODY SIZE from the first commit — 25px where they should be 15. That is most of why the slides read as cluttered. Qualified all three as `.slide p.<class>`. Bigger type means less fits, and that was paid in words rather than by shrinking back: trimmed the prior-art rows, compressed the three-dies logs to two lines per die, moved the DMA figure off the tire slide, and folded a duplicated caption into the honesty note. Verified at 1180x820: 0 slides overflow, 0 code blocks scroll sideways, 0 overview thumbnails spill. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
TYPE. Measured again after the first pass was still too small. Body text on a slide should be ~4% of slide height; mine was 3%. Raised sixteen steps of the scale — at 1180x820 body 25 -> 34px, code 18 -> 26px, h1 52 -> 69px — and paid for it in words rather than by shrinking back: trimmed prose on ten slides, cut the six-faces paragraphs to phrases, compressed the three-dies logs to two lines per die, dropped a redundant closing line on the gates slide. RECORDING. Slide 5 now has a "run it" button that replays a real asciinema capture of the dissolve: wasm-tools shows the component's WIT, loom optimizes, synth lowers to a Cortex-M3 object, then nm and size answer the slide's claim with `U read32 / U write32` and `text 1726 data 0 bss 0`. Recorded by actually running it — the wdg-thin driver had to be rebuilt first because the checked-in target/ wasm was a stale pre-componentization build importing env::mmio_read32. Written as a ~90-line player rather than pulling in a library: the capture contains only SGR colour escapes and newlines (verified — no cursor motion), so append-only rendering is faithful, not an approximation. Text stays selectable and crisp at any projection size, the file is 1.7 KB, casts are fetched once at load so clicking mid-talk never touches the network, and a missing file disables the button instead of breaking the slide. Two bugs fixed on the way: - the terminal <pre> had min-height:0 inside a flex column, so siblings squashed it to a few pixels — you saw the first commands and nothing else. It now claims its space, and "run it" hides the flow diagram so the recording gets the whole slide. It auto-scrolls, ending on the payoff. - `.slide p` (0,2,0) beat `.slide__act` and `.slide__cite` (0,1,0), so the act eyebrow and every citation had rendered at full body size since the first commit. Qualified as `.slide p.<class>`. Playback stops and resets when you leave the slide, so it never runs unseen. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…OS itself
The recording covered only loom -> synth, so it silently skipped the first two
rows of the very slide it sits on. Re-recorded against the real 5-provider
composition, and against the OS rather than a single driver:
wac compose 5 components -> 1 component, 20741 B
exports 5 gust:os, imports mmio + taskdisp
meld fuse 11 memories -> 1 core module, 9874 B (-52.4%)
loom optimize
synth compile -> gustos.o
nm -u -> poll-task, read32, write32
size -> text 4812 data 0 bss 0
The whole gust OS as one relocatable object with a three-symbol trusted
surface and zero SRAM. That is a better demonstration than a driver was.
Flow rows re-stated from those measurements rather than from memory: the
slide had claimed "5 linear memories -> one shared memory" where meld
actually reports 11 -> 1 core module at 52% smaller, and the "3 native
functions" claim is now the measured undefined-symbol count, not an estimate.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…cost The componentization slide named a +700-1100 B canonical-ABI overhead and left it there. It now also shows what we did about it: our wit-bindgen fork's cabi-realloc-extern backs cabi_realloc with a bounded arena that traps instead of growing, worth -318 B (-18%) on wdg-thin, 29% of that driver's overhead. Measured today with the version bump controlled for — the fork is at 0.58, and a naive comparison against the shipped 0.52 would have mis-credited the feature. The slide says the drivers do not use it yet, because they do not. Turns a slide that admitted a cost into one that shows the loop closing: name the cost, patch the tool, measure the result, state what is still undone. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
Scanned every slide for anything crossing its padding box, at five viewport shapes. Two real edge overruns (trailing code comments, 35px and 101px) and, more importantly, a whole class of failure the earlier per-slide trimming could never have fixed. The type was sized in vmin, which tracks min(width, height). On a 16:10 screen that is the width, so body text landed at 2.9% of slide height; on a 4:3 screen vmin IS the height and the same rule gave 4.2%. Slide fit is height-bound, so the denser slides overflowed on 4:3 and 1920x1080 while passing on 1180x820 — and hand-trimming for one shape re-broke another. Each size is now capped against vh at ~0.79 of its vmin coefficient, pinning every aspect to ~3.3% of slide height and letting vmin bind only in portrait, where height is abundant. One lever (`--fs`) remains for a floor on very short laptop screens. Long code lines wrap rather than scroll below 900px, so a tablet held in portrait never hides the end of a line behind a swipe. Measured after, zero overflowing slides and zero elements crossing an edge: 1024x768 body 25px 3.3% 1180x820 body 27px 3.3% 1366x1024 body 34px 3.3% 1920x1080 body 36px 3.3% 820x1180 body 34px 2.9% (portrait — vmin binds, as intended) Also dropped the closing line on the gates slide; the pull-quote already says it and it was the one item still overrunning at every size. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
The factory act described the toolchain as six cube faces, which is an abstraction. synth's own architecture overview is better: it shows WHERE evidence enters, block by block, and it is the project's own diagram rather than one invented for a slide. Six stages — upstream/untrusted, front, middle, back, per-compilation, out — with the evidence-producing and evidence-checking blocks tinted and the one hazard block in amber: trap re-introduction, because hardware is more total than Wasm. That amber block is the most honest thing in the deck's middle: a diagram that is all reassurance is not a diagram anyone should believe. It also closes a loop with the cost slide. The FRONT column carries `cabi arena bind` — wit-bindgen's dangling realloc import resolved to a defined function — which is exactly the mechanism measured at -318 B two slides later. Fitting it took the diagram its own scale, since a diagram is read rather than declaimed: six columns across 1180px put the block labels at 11px, so it flows 3-across into two rows and the labels land at 18px with 15px sub-labels. Diagram slides also get a smaller heading and tighter stacking than prose slides. Verified at 1180x820: 22 slides, none overflowing, nothing crossing an edge. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
Two problems with the first attempt, both real. READING ORDER. The source diagrams are left-to-right stage columns. Six of them on a slide put the block labels at 11px, and reflowing 3-across into two rows destroyed the one thing a pipeline diagram has to convey — which way it goes. Stages are now ROWS with the stage name in a left gutter: one unambiguous top-to-bottom order, and every block gets real width. Block labels 19px, sub-labels 16px (was 11/9). ONLY SYNTH. The talk is about the whole factory, so the slide carried one tool's internals. meld, loom and synth each publish an architecture in the same visual language, so the slide now has a tab per tool and switches instantly — all three stay in the DOM, nothing fetched. What that buys is the alignment across them, which is worth more than any one diagram. Each names one hazard, and they are the same mismatch from three sides: meld Validates != correct tool lenient · engine strict · run exact loom Total-operation model the verifier does not see traps synth Trap re-introduction hardware is more total than Wasm loom's note states it plainly: Wasm is partial, and everything on both sides of it is total. A compiler must put traps back; an optimizer must stop taking them away. Same mismatch, opposite directions, both silent-wrong. Verified at 1180x820: all three tabs fit with zero overflow, and no other slide in the deck overflows either. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
SLIDE 14 asserted a fact channel without ever showing one. It now carries a real wsc.facts payload, computed from loom's own emitter (loom-core/src/lib.rs build_wsc_facts_payload) rather than invented — schema v1, one value-range fact, LEB128, nine bytes total: 01 schema v1 · 01 one fact · 01 kind=value-range 03 func_index · 07 value_id · 03 00 ff 0f body: 0 <= v <= 2047 Nine bytes is the point: the whole proof-carrying channel is smaller than the sentence describing it. The value_id annotation carries the design argument — keyed to a VALUE, because an optimizer renumbers everything, and a fact keyed to a position is still true of something while being asserted about something else. Added loom's own honest scope: emitter and wire format are done and byte-verified against the consumer, but the source that would populate it at volume is not wired, so 232->104 is what the channel does when it carries a fact, not evidence that we produce many. SLIDE 15 gave three numbers and no mechanism — and mixed ratio directions, so 1.65x read as an improvement when it is a regression. It now shows the actual function: gust_mix(ch) = clamp(1500 + (ch - 1024), 1000, 2000) LLVM must emit the clamp because it cannot know ch. The OS primitives above carry a proven bound, ch in [524,1524], so ch+476 is provably inside [1000,2000], both clamp branches are dead, and the function collapses to `add r0,#476; bx lr`. Ratios are now stated in words — 1.4x SLOWER today, 2.2x FASTER with the proof — against a stated unit, so the direction cannot be misread. That is the whole thesis in one function: not out-optimizing LLVM, but optimizing with information LLVM structurally never had. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
CONTROLS — my bug, and a bad one for a presenter. The nav was dimmed to .35 opacity under `@media (hover: hover)` and restored on hover. An iPad with a keyboard or trackpad attached MATCHES that query while the person is still touching the screen, so the controls faded to near-invisible with no hover available to bring them back. They are now always visible (.8, full on hover/focus). A presenter always needs the controls; a little visual noise is the correct trade. SPLIT — 22 -> 29 slides. Six slides were carrying two ideas each: the pipeline flow | running it the wdg contract | the proof that the transition is impossible the wsc.facts bytes | why a value and not a position | what it is worth the clamp-elision example | the measured numbers the componentization cost | the patch that recovers 29% of it the browser shim | the silicon side Each half now gets a slide. Measured after: average fill 62% of available height (was crowding 100% on the worst), nothing overflows, densest slide 82%. 29 slides against a 25-minute slot is ~52s each, which suits slides that carry one idea rather than three. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…eds no server FONT BUG, and very likely the "works in Safari, not Edge" report. `_fonts.scss` self-hosts the Atkinson faces, but it was never imported into main.scss — zero @font-face rules in the compiled CSS. The site got away with it because base.html also links Google Fonts; the deck template does not, so it silently fell back to system fonts: SF Pro on Safari/macOS, Segoe UI on Edge/Windows. Same HTML, different metrics, different look. Importing it gives 18 @font-face rules and the deck now actually renders in the face it was designed for — the same one on every browser. It also closes the privacy regression `_fonts.scss` exists to prevent: the file says in its own comment that self-hosting eliminates the Google Fonts auto-load that transmits visitor IPs, and that elimination had never taken effect. SINGLE-FILE EXPORT (tools/bundle-talk.py). A presentation should not depend on a working local server, on the browser not upgrading a plain-HTTP LAN address to HTTPS, or on anything between the laptop and the screen. The bundler inlines the stylesheet, all 18 fonts as data URIs, and the terminal recording, producing one 632 KB HTML file with ZERO external or absolute references that opens from disk, offline, in any browser. The player prefers an inlined recording over a fetch, which fetch() would refuse on file:// anyway. DRONE SLIDE. Pays off the forward reference on the bias slide. A drone is a car with four rotors instead of four tires: the flight stack and the building supervision system are built from the same ten no_std stream-transformer crates, the same WIT packages, the same component rules, the same traceability gate. And stated at the same resolution as the claim — neither has flown, neither has shipped to a home, and the flight dossier says so itself: "no claim of flight is made anywhere." Aim, not result. 30 slides, none overflowing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
Ran the deck past six reviewer personas built from the venue's own programme plus three domain reviewers (military avionics DAL-A, automotive ASIL-D, robotics real-time). Five reported. Every claim below was checked against the repo before changing anything. CORRECTED — overclaims, in the deck's own honesty terms: - `irq` was listed under "what touches metal" beside dma/uart, which reads as interrupt support. The WIT is `poll: func(line: u32) -> bool` — no handler registration, no vector ownership, no ISR path. Now says so on the slide. Flagged as the deck's most misleading square centimetre, by omission. - "WCET sidecar / sound per-function" — the sidecar reports 9 DECLINED against 4 bounded, declines on any call (intra-procedural), and assumes zero-wait-state instruction memory, while the same slide lists M7/A53 backends where that assumption is fiction. Now "leaf functions only · declines on call". - "The pipeline is qualified once; every product that uses it inherits that qualification" — categorically false under DO-330 and ISO 26262-8. Credit is granted per project against user-written tool operational requirements; data is reusable, credit is not inherited. Now "qualify once, and the ARGUMENT amortizes", which is true and loses nothing. - 1.839x was tinted green. It is an 84% slowdown. Now amber, and says "slower". - "0 SRAM" on the fused OS -> ".bss 0". Zero .bss is the real and strong claim; "no RAM" is not, and the first question about task stacks collects the slide. - The `+ wsc.facts` arrow was drawn as populated while a later slide admits the producer is not wired. The pipeline slide now says so where the arrow is. - Two wdg baselines on adjacent slides (1726 B vs 1746 B) were different builds presented without explanation. Labelled. - Added the line the driver-cost slide was missing: flash is cheap on these parts, SRAM is the binding constraint, and .data/.bss stay 0 -> 0. REJECTED — one reviewer claim did not survive checking. The avionics persona said synth has no WCET support and the deck should delete the chip. But emit-wcet.sh documents `--emit-wcet`, schema synth-wcet-v1, synth >= 0.46.0 (synth#778); their checkout predates it. Their SUBSTANTIVE point — that the bound is intra-procedural and model-relative — is correct and is what the reworded chip now says. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…e gates exist The site's own tagline is "AI writes the code. Who proves it's safe?" and the deck never said it. The entire factory — oracle gates, per-compilation validation, typed traceability, the five green-for-the-wrong-reason findings — exists BECAUSE an assistant will produce a plausible driver, a plausible proof and a plausible green test faster than anyone can read them. Omitting that left Act IV looking like unusual diligence rather than a necessary response. New slide before the factory quote: the premise stated plainly, and the pivot that follows from it — the question stopped being "can it write the code" and became "what would have to be true for me to believe it." It also sets up the failure slides as the interesting part rather than as an apology. Also disambiguates the two wdg baselines (1746 vs 1726) on the slide itself. Three separate reviewers pulled that thread, and in a deck whose title slide promises "every number says where it came from", a 20-byte unexplained discrepancy is the one loose end that unravels the rest. 31 slides, none overflowing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
As slide 4 it was a claim, and an industrial reviewer's verdict was that it "spends credibility to buy nothing" that early: an audience hears two unshipped verticals before it has been given a reason to believe anything. As the penultimate slide it is an outlook, which is what it actually is — and the honesty stops being a retraction and becomes a destination. Retitled "Where all of this is aimed", and the not-yets are now a ledger rather than a caveat buried in a caption: has not flown, has not shipped to a home, the board is on the bench and not in the air. Adds what the earlier version omitted — the hardware-integration hub exists, pins its input by hash, and runs the whole meld -> loom -> synth chain per upstream release. That is the concrete thing the substrate is aimed at, and it is the strongest supporting evidence for the claim the slide makes. Its dossier's own sentence closes it: "no claim of flight is made anywhere." Everything earlier in the talk is work toward this, and none of it is this yet. Act I's forward reference now says "I will come back to that", and it does. 31 slides, none overflowing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…he LLVM point FALSIFIED OUR OWN CLAIM. The deck said "a compiler with no verifier cannot reach it." Measured: told the premise via core::hint::assert_unchecked, stock LLVM folds the clamp identically (30 B -> 12 B, add.w r0,r0,#476). The claim is gone. What replaced it is stronger, and it is the question the whole deck is about: assert_unchecked is UNCHECKED. You can tell a compiler anything and it will believe you; get the range wrong and it is undefined behaviour, silently, with no diagnostic. So both paths emit the same instruction and only one of them checked. The result was never the codegen — it is the provenance of the premise. "How would you know the premise is true" is the same question as "what would have to be true for me to believe it", which is now the deck's stated premise slide. ADDED — what you still have to trust. Four of six reviewers independently reconstructed a trusted base because the deck had none, and ".o + 3 native functions" invites the misread that the TCB is three functions. It now lists what the gates do not cover, and says outright: three native functions is the seam, not the trusted base. ADDED — when NOT to dissolve. The line where a shared system-interface binary is the right answer instead: several runtimes per OS+ISA, wide dynamic interfaces, third-party binaries, field update without re-qualifying the image. Naming the opposing position as correct on its own side of the line is worth more than arguing against it. CUT — "Six faces, not four tools" (a product tour of ten proper nouns this audience does not know; the architecture slide carries the real content) and the self-quotation slide (a full slide citing our own blog as authority, in a deck whose entire strategy is evidence). The qualify-once sentence survives on the premise slide where it belongs. FIXED — the mixer slide now says the output clamp stays and the bound comes from a verified primitive rather than off the wire. Two reviewers read the old version as deleting a failsafe on untrusted input. 31 slides, none overflowing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
Tried it as slide 4 (read as an unshipped claim before the audience had reason to believe anything) and then as the penultimate north star. It does not earn its place either way: the substrate's cross-domain reach is a supply-chain claim about shared crates, and the talk never needed it to make its argument. An industrial reviewer's verdict on the early version was that it "spends credibility to buy nothing", and moving it did not change what it bought. Also removes the forward reference it left behind: the bias line now stands on its own, which is stronger — declaring the automotive bias needs no follow-up promise. The deck now closes: two things building this talk taught us -> before the rest of the vision holds -> when not to dissolve -> change the tires, not the car. Ending on where NOT to use this, immediately before the title line, is a better last impression than an unshipped vertical. 30 slides, none overflowing, ~50s each against the 25-minute slot. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…y lands The bias line sat on slide 3, under a split about portability layers, where it was orphaned from the thing it explains. But the title IS the metaphor — the moment "Change the Tires, Not the Car" is on screen, a room of compiler and formal-methods people is already holding the "why cars?" question. Answering it two slides later means they sat with it through the prior-art slide. On the title it also pairs with the other declaration already there: the bias and "every number on these slides says where it came from" are the same kind of statement — here is my position, and here is how to check me. Two declarations, one slide, before any claim is made. 30 slides, none overflowing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
… errors Wrote the deck's factual claims as 40 falsifiable statements and had them checked by a verifier briefed cold, told to measure rather than trust any document's assertion about itself, and told that cannot-verify beats a guess. Six refutes. Five stand; four were mine, introduced in this session. REFUTED AND FIXED: - "11 linear memories" -> 5. My own count: I grepped `(memory ` and hit 5 declarations plus 5 `(export "memory"` lines plus one `canon lift (memory $m)`. meld's stdout says "Fusing 11 components", which made the wrong number look right. FUSED-GUSTOS.md says plainly "Linear memories: still five". - spi 454 -> 1244 B. Refuted: 1244 appears NOWHERE in the repo or its history. The measured and recorded figure is 1450 (spi-thin/RESULTS.md:71, and a rebuild agrees). - wdg 638 -> 1726 B. The committed componentized object is 1718; 1726 is only reproducible as a synth-0.49 rebuild. Cost slide now uses the shipped 1718, and the patch slide says its control is a rebuild rather than the shipped object. - USART driver 326 B -> 254 B. The committed uart-thin-cm3.o measures 254/0/0. 326 comes from RESULTS.md attributed to loom 1.1.16 + synth 0.15.0, a toolchain two years stale; no build reproduces it today. - `add r0,#476; bx lr` as "the whole function". The measured codegen is five instructions and 12 bytes, including uxth and a frame push/pop. COMPARE.md labels the two-instruction form "what synth COULD ship (synth#494a)" — an aspiration I had put on a slide as a measurement. REFUTE REJECTED: the verifier found no "we have not been audited" statement and refuted it. It searched gale; the sentence is on the website (templates/about.html:58 and :89, "We will tell you when an authority audit happens; we have not been audited yet"). Claim stands. ALSO CORRECTED, in our favour: "Proofs run on a schedule, not every commit" was wrong in the pessimistic direction. Verus, Rocq and Kani ARE gated on push and pull request to main — path-filtered, so a commit outside those paths triggers nothing. The real gap is narrower and sharper: Lean runs in no workflow at all. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
It said "OS written for the chip. Application hoped to be portable. Every new board re-opens the OS." — a caricature, and weak precisely where the argument needs to be strong. An audience with embedded experience hears a caricature and discounts everything after it. Retitled "How embedded actually builds software", and now says what, why and how: WHAT — the vendor's HAL and board-support package for that part; an RTOS with a port layer per architecture and a board file per board; register headers generated from the chip's own description file; #ifdef for variants; one statically linked image. WHY — and it is the right answer. No MMU. Kilobytes of RAM. Hard deadlines. Cents per unit. Every abstraction costs bytes and cycles that are not there, and the vendor knows the silicon better than you do. It works. Then the consequence, which is the only part actually worth arguing about: the OS is the layer that gets rewritten per target, and the application's portability is a convention rather than a contract. Conceding that the incumbent is correct under its constraints is what earns the right to propose a different one — and it makes the inversion a response to a real cost rather than a claim that everyone else was doing it wrong. No vendor or product names, per the standing rule; all of it stated generically and factually. 30 slides, none overflowing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
Walked all 30 asking one question per slide: does this carry enough to explain
what it is, or to set up the thing it demonstrates? Six could not.
- 6 "The same chain, actually run" was a heading and a button — twelve words. If
the recording is not played, or it fails, the slide says nothing at all. It now
states what you are about to watch and, more importantly, the two questions the
run answers: what does the object still need from the world, and what does it
cost.
- 8 showed `interface wdg { unlock · configure · lock ... }` — names separated by
dots. That is prose in a code box, and in a room full of Component Model people
it discounts the entire contract argument. Replaced with the real WIT, six
function signatures, verbatim from gust-hal.wit.
- 12 opened on JavaScript with no framing. It now says what the shim IS — the
answer to an imported interface — before showing it.
- 19 said "a bounds-guard sequence", which is unfalsifiable as written. Now "one
guarded memory access, lowered with and without the fact".
- 22 gave "62 / 62" with no denominator, which is a ratio chosen to be 1.0. Now
carries its own scope row: 62 of the BIT-VECTOR obligations, and the rest of
each proof still rests on the solver.
- 24 listed five verification failures in five cryptic lines and explained none.
One is now worked through concretely — a requirement said the fuser rejects a
component that instantiates a module twice; the test called the reject function
directly and passed; the shipped path accepted those modules and duplicated
them. That is the one that generalises, and it is what makes the pull-quote land.
30 slides, none overflowing, nothing crossing an edge.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
Rows like "2022 | lowered ahead of time, no engine | x86-64" named no work and no group, so they read as "prior art exists, in the abstract" — and the right-hand column silently reduced each prior result to its deficiency relative to this one. Two reviewers said an unattributed year-row is worse than no row. Fixing it meant naming four talks, which brushes the standing rule on third-party names in public artifacts, for a slide that was not carrying its 50 seconds. Cut rather than repaired. Crediting the adjacent work verbally costs nothing, is more generous than a ledger row, and can name the delta properly — which is the part that was wrong anyway: the interesting difference was never the instruction set. Nothing depended on it — checked for references to "four ingredients", "all four at once", "two hours ago" and the named analysis; zero hits. 29 slides, none overflowing, ~52s each. Act I is now a single slide, which suits it: the inversion is one idea and the deck gets to the seams faster. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
Each tool publishes its architecture with its own stage vocabulary — meld says Parse/Resolve/Merge/Adapt/Out, loom says In/IR/Passes/Per-compilation/Gate/Out, synth says Upstream/Front/Middle/Back/Per-compilation/Out, scry says In/Value-domains/Relational/Memory/Fixpoint/Out. Four names for the same five things, which made the slide look like four unrelated tools. They are now one spine — in · model · work · check · out — identical rows in all four tabs, so switching tools compares like with like instead of asking the room to re-learn a vocabulary three times. scry added as the fourth: verified premises in, ten abstract domains as the model, the fixpoint as the work, 19 Rocq files with 0 admits as the check, and out the shadow-stack bound that synth consumes plus a gap report of every ⊤ as data. The unification pays off in the hazard row, which is the real result. All four name exactly one hazard, and it is the SAME defect four times — each tool's model is more total than Wasm: scry wrapping arithmetic Z is not i32 loom total-operation model the verifier does not see traps synth trap re-introduction hardware is more total than Wasm meld validates != correct the validator is lenient where the machine is exact Wasm is partial; mathematics, SMT, silicon and validators are all total. That is a property of the specification's neighbours rather than of any one tool, and it is worth more than any single diagram on the slide. Verified: identical five row labels across all four tabs, one hazard each, zero overflow on every tab. 29 slides. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
The tabs read meld / loom / synth / scry — four names this room has no reason to
know — and the rows below them are structure, not purpose. The slide said HOW
four times and never once said WHAT. Selecting a tab now swaps a plain-language
line in above the diagram:
meld welds many components, joined at their interfaces, into a single
module — so the boundaries stop existing at run time
loom rewrites the code to be smaller and faster, and reverts any rewrite it
cannot prove keeps the same behaviour
synth turns the wasm into real machine instructions for a real chip, and
re-proves the translation on every compilation
scry reads the code without running it and works out what can and cannot
happen — recording every place it had to give up
Each is the tool's actual contract in one sentence, and each carries the thing
that makes it unusual: loom REVERTS what it cannot prove, synth re-proves PER
COMPILATION, scry records where it GAVE UP, meld makes the boundary stop
existing. Someone who reads only these four lines has the talk's argument.
Verified per tab: exactly one description and one row-set visible, both matching
the selected tool, zero overflow on all four. 29 slides.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…ing the incumbent The old Act I slide was a split: "the usual arrangement" beside "what we are trying". Rewriting it into the traditional-embedded steelman replaced BOTH columns, so the second one — the actual proposal — was silently dropped. The deck then went from "here is how embedded builds software today, and it is the right answer" straight into WIT interface listings, with the thesis missing from between them. Caught on a read-through, not by any check I had. New slide 3, "So invert it": write the OS itself as WebAssembly components and make the Component Model the integration step — between OS components, between the OS and its drivers, between the OS and the tenants above it. Not a runtime on the device: a build step that joins typed pieces and then gets compiled away. Then the car and the tires, which is what the title has been promising since slide 1 and which nothing had yet cashed. It also gives slide 4 something to be the answer to: "two seams, and everything hangs off them" only means something once the room knows the OS is supposed to be made of components. 30 slides, none overflowing, ~50s each. Act I is two slides: what everyone does, and what we do instead. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
The pipeline read `wac compose · meld fuse · loom optimize · synth compile · ld`. Those names mean nothing to this room, and the slide that explains them is 16 — eleven slides after the one that depends on them. The audience was being asked to follow a chain of four unfamiliar proper nouns before being told what any of them do. The stage column now leads with the ACTION and demotes the tool to a sub-label: compose (wac) -> fuse (meld) -> optimize (loom) -> lower to ARM (synth) -> link (ld) Anyone can follow compose, fuse, optimize, lower, link. The names are still there for whoever wants to go and find them afterwards, which is the only thing they were ever needed for on this slide. Added the sentence the slide was missing: five components in, one native object out, and every arrow happens on a build machine rather than on the device. That is the whole claim of the slide title, and it was only implied by the diagram. 30 slides, none overflowing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
The verb/tool split shipped with markup but no style: the sass edit that was
supposed to add `.flow__stage small { display: block }` silently matched nothing,
because an earlier pass had already rewritten that block's font-size to the
vh-capped form. String replace found no match, wrote the file unchanged, and
reported success — so `<small>wac</small>` rendered inline and the stage read
"composewac".
I checked the markup and the measured slide fit afterwards, and both were fine.
Neither of those could see the defect: the element was present, the slide did not
overflow, and textContent concatenates without whitespace anyway, so my own
verification printed "composewac" and I read it as expected output rather than as
the bug.
Rule now applied against the block as it actually exists, and verified where it
matters — computed display is `block` on all five, and each tool name measures on
its own line beneath its verb:
compose (wac) · fuse (meld) · optimize (loom) · lower to ARM (synth) · link (ld)
30 slides, none overflowing.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
New slide, "The part sets the rules", right before the seam. It carries the geometry (128K flash / 8K SRAM, generated from the AADL model rather than hand-written) and then the number the deck was missing entirely: a whole flashed image on that part is 6 028 B of flash and EIGHT BYTES of SRAM, leaving 8 184 free. This reframes the rest of the deck. "0 SRAM drivers", "no engine", scalar-only interfaces and an allocator that traps instead of growing all read as taste until the audience knows the part has 8 KB — after which they read as consequences. Three reviewers reached for this independently: the automotive one said the componentization tax is fatal exactly on this part class and noted our demo dies ARE that class; the industrial one said zero static RAM is the number that matters and it was sitting on a slide titled "what componentizing costs" as the consolation prize. Scope on the slide and in the repo note: this is the watchdog silicon test image, one dissolved driver plus the minimum to boot and report — a floor, not a system footprint, with no scheduler, task set or application in it. 31 slides, none overflowing, ~48s each. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…st board we had I had framed the F100 as "the part that sets the rules" — true, but it read as a size stunt. It is the FAILSAFE: the IO-MCU beside the main flight computer, forwarding per-motor commands. If that computer stops, this is what is still driving the motors. And its safety property came from a real failure. It must forward commands BYTE-EXACT — no re-mixing, no per-motor floors — because when a rotor fails and the controller asymmetrically zeros motors, re-mixing reintroduces the parasitic moment that caused a real failure in a prior release. The oracle is 184 checks, 46 rows x 4 motors, byte-exact, with a negative control that MUST fail: a symmetric averaging re-mix has to be rejected. That changes what every constraint in the deck means. "0 SRAM drivers", "no engine", scalar-only interfaces, an allocator that traps rather than grows — all of it read as taste when the part was anonymous. Attached to a controller whose job is to keep an aircraft flying after a motor dies, they read as consequences. Split into two slides because the two ideas are separable and each is a full thought: what the part IS and what its property is, then what an image costs on it (6 028 B flash, 8 B SRAM, 8 184 free), with the scope stated — one dissolved driver plus the minimum to boot, a floor and not a system footprint. 32 slides, none overflowing, ~47s each. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…slide The slide asserted the pass-through property as prose, which in a deck arguing that traceability is the point was the wrong way round. It is defined as a typed requirement: the three-core partition (flight cascade on the M7, estimator on the M4, failsafe on the F100), PART-P02(a) pass-through fidelity, its WIT generated from the architecture model rather than hand-written, and an oracle gating it — 46 rows x 4 motors, byte-exact, with a negative control that must fail. That is the factory applied to the car, and it closes a loop the deck had left open: Act II shows the artifact, Act IV shows the machinery, and until now nothing said the machinery had produced this particular artifact. Status stated on the slide: DRAFT. The requirement is specified against a future release, not delivered — and in a deck whose title slide promises every number says where it came from, a specified-but-undelivered requirement has to say so where it is claimed, not in a backup slide. 32 slides, none overflowing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…our word Checked what the toolchain actually claims. gale's OS-node builds pass `synth --shadow-stack-size 2048`, and synth's own flag contract says exactly what that means: "The footprint is ASSERTED (the budget is trusted), not proven — synth does not yet prove the program's max shadow-stack depth fits the budget (that is the layer-2 auto-proof / scry tail)." So on a part with 8 192 bytes of SRAM we reserve 2 048 of them on an assertion, and the deck did not say so — while spending two slides on how little SRAM the drivers use. That is the wrong side of the ledger to be quiet about. The gaps slide now names it: an OS node reserves 2 048 of those 8 192 bytes, the compiler's contract says the budget is asserted rather than proven, scry computes the depth, and wiring it to the reservation is the named next step. Until it lands, the number is our word. This is also the specific answer to a reviewer's "no stack bound, no ASIL-D" — the honest position is not that we have the bound, it is that we know exactly which tool produces it and exactly what is missing between here and there. Noted while checking, not put on a slide: synth ships `--stack-layout low`, which places the stack at the bottom of SRAM so an overflow BusFaults on the first errant push instead of silently corrupting globals — no MPU needed. It refuses on relocatable, host-linked images, which is precisely our path, so the harness owns that layout and we do not get the protection. Worth a look separately. 32 slides, none overflowing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
Asked whether slide 23 should mention the assert_unchecked result. Checked: it
was not on 23, it was not on 22, it was not in the deck at all. Splitting the
clamp slide into mechanism + numbers dropped it, exactly as splitting the Act I
slide dropped the inversion column earlier today. Third time a string-replace
edit has silently lost content in this session, and this time it took the single
best line in the deck.
Restored as its own slide, which is where it belonged anyway — the objection
forms the instant the numbers table claims 2.2x against native LLVM, so it should
land on the very next slide rather than be folded into either neighbour:
assert_unchecked(524 <= ch && ch <= 1524);
-> add.w r0, r0, #476 stock LLVM, 30 B -> 12 B
"So the codegen is not the result. Both emit the same instruction — only one of
them checked."
"You can tell a compiler anything and it will believe you. Get that range wrong
and it is undefined behaviour, silently, with no diagnostic. The question was
never CAN the compiler fold it — it is HOW WOULD YOU KNOW the premise is true."
Verified by rendering rather than by grep: the source greps as zero for
"assert_unchecked" because the markup splits the token, which is precisely the
kind of false negative that let it go missing in the first place. Confirmed
present in the rendered DOM, on slide 24, with no overflow.
33 slides, none overflowing.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
HIGHLIGHTING. Eight source blocks now carry data-lang (wit, rust, js, sh) and get
tokenised. Captured output, hexdumps and measurement tables deliberately do NOT —
colouring evidence like code misrepresents what it is.
The highlighter rewrites only the DIRECT text-node children of a tagged block, so
the hand-authored spans marking results (.ok/.dim/.hi) are never touched or
nested into. First version ran its rules in sequence over a string that was
accumulating markup, so `str` inside `class="tok-str"` matched the Rust type list
and corrupted two blocks into `class="tok-ty">Uint32Array`. Rewritten as a single
non-rescanning tokenizer pass with keyword sets. Verified: 0 corrupted blocks,
0 untagged blocks touched, manual spans intact.
DMA RESTORED. A history sweep for content silently lost to my slide edits found
exactly one real casualty — the DMA ownership figures — and it left `dma` as a
bare unexplained word in the gust:hal list, which is what prompted the question.
It is back, and it is the strongest Component Model content in the project:
resource dma-buffer { len: func() -> u32; }
read: func(channel: u32, buf: dma-buffer) -> future<dma-buffer>
Consuming own<dma-buffer> makes the buffer statically inaccessible to wasm until
the future resolves with the re-owned handle; circular DMA is a stream of
per-chunk ownership, each chunk owned by exactly one side at a time. 220 B,
0 SRAM, 6 Kani proofs.
That block uses resource, own, future AND stream — the exact question a Component
Model audience asks about a deck whose every other interface is scalar. Corrected
against the artifact while restoring it: the object is 220 B, not the 218 I had
been carrying.
34 slides, none overflowing.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…th no source Slide 20 opened "When loom proves a value range it does not discard it" and never said how loom knew the range. A room that has just been told to distrust every stage will ask, and the honest answer is better than the omission: "It is not running a separate pass to hunt for facts. To delete a bounds check it must already have established the index is in range — every optimizer does that. What is unusual is what happens next: normally the code is emitted and the reasoning that justified it evaporates." That reframes the contribution. It is not extra analysis bolted on for our benefit; it is declining to throw away work the optimizer already had to do to justify its own rewrite. Which is also why the cost of the channel is nine bytes rather than another analysis pass. 34 slides, none overflowing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…esented today Our upstream analyser and the bounds-check work presented earlier the same morning are the same family of technique on the same problem. Saying so is the strongest move available, because the comparison is unflattering in the places that matter and admitting that is what makes the rest credible: their output contract is cleaner (a flat list of provably-safe offsets any runtime can consume), they handle a branch shape ours misses, and they measured an end-to-end speedup we have not. And it turns the deck's biggest admitted gap into an ask. The previous slide concedes that the source which would populate the fact channel at volume is not wired. That analysis produces exactly those facts. Both projects are about two months old. Better than a prior-art ledger row: it credits by contribution rather than by year, names what they do better, and ends in a collaboration rather than a comparison. NOT added, because it is not true: a claim that we implemented RFC-46. Asked whether to mention it, checked, and meld's own RFC response says "On multiply-instantiated modules: we currently reject these" — corroborated by commit 2137398, "already mitigated by reject", and by the absence of any implementation in the crates. What exists is a considered response from an independent implementer, offering 45 canonical-ABI fixtures, edge cases found through debugging, and Rocq proofs as a reference specification. That is worth saying out loud in Q&A; "we implemented the RFC" is not. 35 slides, none overflowing, ~43s each. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
… subset
I said we had not implemented RFC 46. That was wrong, and it was wrong in the way
this deck is about: I read one section — "on multiply-instantiated modules: we
currently reject these" — and generalised a local negative into a global one
without reading the rest.
The response's own opening says meld "does essentially what this RFC proposes for
the sync subset of the component model", and that "the core architecture matches
what this RFC describes: parse components, flatten the composition DAG, merge
index spaces, generate FACT-style adapter trampolines, wrap the result back into
a P2 component for host compatibility." Multiply-instantiated modules is one
question inside the RFC, not the RFC.
New slide, "Is this the Component Model, or our dialect?", which is the question a
CG audience asks first and the deck had no answer to:
43 / 45 canonical-ABI fixtures pass at runtime — strings, lists, records,
variants, options, results, resources, flags, enums, both directions
declined async / fibers — no stack switching on these parts, and compiling the
runtime in is a TCB problem
rejected multiply-instantiated modules — refused rather than shipped as an
unproved transform
with the two known failures named: three-component resource chains where an
intermediate re-exports a resource it does not define.
That is a far better answer than either "we follow the spec" or my previous "we
did not implement it" — it is a conformance ledger, with the declines stated as
choices and the rejection stated as a refusal to ship something unproven.
36 slides, none overflowing, ~42s each.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
With tool names running through the deck, "is this slide about meld specifically, or about everything?" was a question the audience had to hold while also following the argument. Each slide now carries a scope chip beside its act label, coloured by kind: accent for a single tool or component, cyan for a set or the whole chain. the whole chain · four tools · five tools · loom -> synth · synth vs LLVM meld · scry · synth · the checker · wit-bindgen gust:os · gust:hal · gust:hal · dma · gust on the F100 · one driver gust, three parts · gust, three hosts · gust drivers everything below the seam · all of it 29 tagged. Seven deliberately not: the title, the two Act I framing slides, the AI premise, the two-things-we-learned slide, when-not-to-dissolve and the close. None of those is about a tool, and a chip there would be noise pretending to be structure. The distinction it draws is the one that actually matters for this deck: a claim about one component is a different kind of claim from one about the pipeline, and several of the numbers only mean what they mean at a stated scope — "43/45" is meld, "8 B of SRAM" is one image on one part, "four tools, one spine" is the set. 36 slides, none overflowing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
Removed: qualify-the-checker (LRAT/Lean/62-of-62), the verification-scope ledger (including "we have not been audited"), the five green-for-the-wrong-reason findings, and the two-things-building-this-talk learnings. That is the entire software-process spine, and cutting it is right for THIS room. Wasm Research Day is co-located with the CG meeting; its currency is results about WebAssembly, not lessons about how a team verifies its work. Those four slides answered questions nobody at this venue asked — "we have not been audited" matters to a certification audience, and "check whether your gate can go red" belongs at a verification-practice venue. Both are true and neither is a wasm result. The test applied was a good one: could this be explained quickly to someone outside the field, and can it be justified at this venue. All four failed both. What it costs, stated plainly: six reviewer personas independently called the green-for-the-wrong-reason slide the best in the deck, and one called it a publishable negative result. It is genuinely strong material — for a different audience, in a different talk. Keeping it as a Q&A answer costs nothing; keeping it on a slide cost four minutes of a twenty-five minute wasm slot. What it buys: Act IV is now the fact channel, the architecture, and the measurement, end to end — which is the wasm contribution. Checked for dangling references to the cut material: none. 32 slides, none overflowing, ~47s each. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
THE ASK. The deck ended on a slogan and a URL — memorable, and nothing anyone could act on or measure. New penultimate slide, "Two things I want from this room", makes both asks concrete and venue-appropriate: the channel is nine bytes and the schema is yours — if your analysis produces value ranges, it already produces the facts it carries; mine has an emitter, a wire format and a consumer, and no source at volume which fragment of the Component Model survives complete ahead-of-time erasure? my ledger is 43 of 45, minus async, minus multiple instantiation — tell me where it is wrong Both are observable within days: does anyone ask for the schema, does anyone engage the erasure question. Neither is "did they find it interesting". Deliberately NOT the ask: "go and check whether your own gate can go red." That is a software-process finding and this is a wasm research day co-located with the CG meeting. True, transferable, wrong venue. BACKUP. The four slides cut for venue fit are restored after the close, marked `backup — not in the talk` with an amber rule so the speaker can never wonder whether they have run past the ending. They are exactly the right backup material, because each answers a question likely to be asked and none of them belongs in the linear 25 minutes: the checker/certificate argument, the verification-scope ledger, the five green-for-the-wrong-reason findings, and the making-of learnings. Press the overview button and jump straight to one. 33 talk slides (~45s each) + 4 backup. None overflowing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…her option "The missing source was in this room this morning" referred to concurrent work without naming it, because I was applying the no-third-party-names rule to a research venue where citing adjacent work is the norm. The result was the worst of both: too specific to be general, too coy to be a credit. It reads as either not knowing whose work it is, or not wanting to say. Cut rather than repaired, because the ask slide added a moment ago already carries the point in its general form — "if your analysis produces value ranges, it already produces the facts it carries" — and makes the same offer to whoever in the room it applies to, without the awkwardness. The specific credit is better said out loud anyway: naming the work, saying what it does better than ours, and that its output is exactly what our channel lacks, is more generous spoken than as a bullet — and it lets the comparison be warm instead of a ledger row. Checked for dangling references to the cut slide: none. 32 talk slides (~47s each) + 4 backup. None overflowing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
The plain-language line said scry "reads the code without running it and works out what can and cannot happen". Accurate, and it threw away the one word that locates the tool instantly for this audience. A wasm research room co-located with the CG meeting does not need abstract interpretation explained; it needs to be told that is what this is. "scry is SOUND ABSTRACT INTERPRETATION — it reads the code without running it and over-approximates, so what it proves holds on every run. It records every place it had to give up as data." Naming the technique also does work the deck lost when the unnamed-credit slide was cut: it puts scry in the same family as the bounds-check work presented earlier the same day, so the verbal credit has something on screen to attach to, and the over-approximation clause says why its output is safe for a consumer to act on. Verified on the tab: line swaps correctly, zero overflow on all four tabs. 32 talk slides + 4 backup, none overflowing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…ime to transact
"Two things I want from this room" was an ask, and the slot has five minutes of
Q&A. There is no room to transact, and after twenty-five minutes of being taken
somewhere an audience should leave holding something, not owing something.
Reframed as "Three things to take with you":
one the Component Model can be a BUILD step — it does not have to be present
at run time; 43 of 45 canonical-ABI fixtures survive complete erasure
two a proof can cross a tool boundary in NINE BYTES — keyed to a value,
dropped rather than re-pointed when the value dies
three on a part with 8 KB of RAM the seam costs nothing at run time, because
by then it is not there
Each is a result the room can check, and each is the payoff of a leg of the
journey: the erasure profile from the meld ledger, the channel from Act IV, the
footprint from the failsafe part.
The ask survives as one line underneath, as an invitation rather than a request:
the schema is open, and the erasure ledger is a claim rather than a result — if
it is wrong I would rather hear it than not. That still produces the measurable
outcome (does anyone ask for the schema, does anyone contest the ledger) without
spending the closing slide demanding it.
32 talk slides + 4 backup, none overflowing.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
New slide 2, "In twenty-five minutes" — by the end you will be able to: say which parts of the Component Model survive being compiled away entirely, and which do not describe how one tool hands a machine-checked fact to the next, and why it is keyed to a value rather than a position quote what an operating system made of components costs on a part with 8 KB of RAM Deliberately the same three as the closing slide, in the same order. The audience decides in the first minute whether to spend attention, and a concrete promise is what buys it — then the close pays exactly that promise back rather than summarising whatever happened to be said. It also gives the middle a spine: every act now visibly serves one of the three, which is a better test for future cuts than "is this interesting". Closing line makes the contract explicit rather than implied: if any of those is still unclear at the end, I have failed — ask me. In a five-minute Q&A that also does useful work, by telling the room what a good question looks like. 33 talk slides (~45s each) + 4 backup, none overflowing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
Thirty-three slides and no author anywhere — an omission nobody had caught, including six reviewer personas and a clean-room verifier, because every check was aimed at whether the claims were true rather than at whether anyone could tell whose claims they were. Title slide now carries "Ralf Anton Beier · avrabe" between the subtitle and the declarations, and the closing slide carries the same plus github.com/avrabe. Both names on purpose: the full name is who is speaking, and at this venue the handle is what someone actually types afterwards to find the work. A talk that successfully persuades a room and then leaves them unable to locate the repo has wasted the persuasion. 33 talk slides + 4 backup, none overflowing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
"say which parts survive" was the odd one out against "describe" and "quote", and it undersold its own bullet. Explaining which parts survive implies knowing why they do; saying them implies reciting a list. The three verbs now escalate, which is what the slide wants: explain the mechanism, describe the protocol, quote the number. explain which parts of the Component Model survive being compiled away describe how one tool hands a machine-checked fact to the next quote what an OS made of components costs on a part with 8 KB of RAM Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…sures SLIDE 8 said "flight computer" and "rotor" without the deck ever mentioning a drone, and put two numbers (128K/8K) inside a 1296px-wide code box that was mostly empty frame. It now opens with the context — we build flight software for a drone, a car in the air with four rotors instead of four tires, and this is its emergency motor controller — and the geometry is a single ledger row instead of a near-empty <pre>. 43/45 — my phrasing on the takeaway slide was loose in two ways, caught on being asked what it actually means. It said the fixtures "survive complete erasure", which implies lowering all the way to native with no runtime present, and it read like a spec-coverage ratio. What the number is: 45 wit-bindgen fixtures, each a component graph exercising one canonical-ABI feature — strings, lists, records, variants, options, results, resources, multi-return, flags, enums, type aliases — in both directions of cross-component calls. meld fuses each graph into one core module, the fused module is RUN, and behaviour is compared against the unfused original. 43 behave identically. So the row now says what was measured: fuse the graph into one core module and the boundary is gone, and 43 of 45 canonical-ABI fixtures then behave identically. The two that do not are named in the footer — resource chains through a re-exporting middle component. A number a listener can act on beats a number that sounds bigger. 33 talk slides + 4 backup, none overflowing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…t mean The title slide promises "every number on these slides says where it came from". This writes that down, as a second page to keep open on another screen during Q&A. Per figure: what the slide says, what it actually measures, what it does NOT mean, and where it came from. Covers 43/45 (slides 19 and 32), the composition figures, the 8-byte image, the 2048-byte stack reservation, the driver seams, the three dies, the fact channel, the clamp numbers, the componentization cost, and the 50 Rocq Qed denominator. It also carries the corrections made while building the deck, on the record and in the speaker's own hands rather than only in commit messages: 11 linear memories was 5 — a grep that also matched export lines spi 454 -> 1244 was 1450 — 1244 appears nowhere in the repo the USART seam was 326 B, is 254 — 326 came from a two-year-old toolchain the DMA object is 220 B, not 218 "a compiler with no verifier cannot reach it" is false — LLVM folds it too the -318 control is a rebuild, not the shipped 1718 object And a closing section of things to volunteer before being asked: proofs are gated on PRs but path-filtered, Lean runs in no workflow at all, and we have not been audited. The point is that a number a speaker can defend under questioning is worth more than a number that sounds larger — and the two failing fixtures, the asserted stack budget and the 1.4x-slower shipping configuration are all easier to say out loud first than to concede second. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…ilure's shape Three corrections the audience would have hit: synth's `in` row claimed "WIT / ABI — lift · lower" and never named the real input. Every build script in benches/gust/ calls `synth compile` on a core module (loom.wasm, fused.stripped.wasm, or .wat); synth's CLI has no --wit flag. It does carry synth-wit and synth-abi, but they are off this path — meld does the lifting and lowering one stage earlier. The row credited synth with meld's work. The cyan/amber coding had no key, and at 8% tint on a cream ground it was not even visible. Both fixed: stronger tints, and a legend on the closing line saying what the two colours mean. "The two" on the ledger now carries the shape of the failure in the value column rather than a paragraph of prose. The figure had to be allowed to wrap — .ledger__val sets white-space: nowrap, which it inherited and which clipped it at iPad width instead of shrinking. Spacing tightened on 6, 21 and 30 so all 37 slides fit with zero overflow at 1024x768, 1180x820 and 1440x900. 6 and 30 were already over at 4:3 before today. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…n an outlook
Three changes, all from presenting-day review.
1. The inversion was described as a METHOD ("write the OS as components") when it is
a CLAIM about how embedded works. Slide 4 now leads with it: in embedded the
hardware defines the software -- pick the part and you have picked the OS, the
drivers, the toolchain -- reverse that dependency, so the software is the durable
artifact and the silicon is a parameter. The car/tires metaphor follows from it
rather than standing in for it.
2. Exact parts instead of shorthand. "F100" -> STM32F100RB (the VLDISCOVERY part,
128 KB flash / 8 KB RAM, geometry generated from stm32f100.aadl) and
NUCLEO-G474RE -> STM32G474RE, so the board and the MCU are not conflated. The
part is now named on slide 8's geometry row, where the 8 KB claim is made.
3. Slides 30 and 31 replaced by ONE outlook slide: "What we are building next, and
what would change our minds." The gaps are not dropped -- they become the thing
being worked on, which is what a research-day room can engage with. Both originals
move to backup, where the earlier cuts already live, so they remain available in
Q&A. The outlook is grounded in the actual release plan: dissolve the whole OS
first (nothing can be verified at object level or bounded until that object
exists), then the stack bound, then isolation on real MPU regions; and the dissolve
is still a trusted step. It closes with what would falsify us.
Deck is now 32 talk + 6 backup. Verified zero overflow and zero clipped elements at
1024x768, 1440x900, with slide 21 checked on all four tabs. Bundle rebuilt (651 783 B,
18 fonts inlined, no external refs). Notes page renamed the part to match.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…ware-defined Three review points from presenting-day read-through. 1. Slide 12 was carrying an acronym the deck never expands. "FSM" appeared EXACTLY ONCE in the whole deck -- in that slide's heading -- and the slide never showed the state machine or named its states, so the audience had to take both the acronym and the object on faith. 2. Slides 11 and 12 were a pair making one argument, and 11 already carried it visually: six functions, no stop. Merged into one slide. The proof survives as the sentence that was actually the point -- the driver is a small state machine, Idle -> Configured -> Running, and a bounded proof shows no edge leaves Running. The Kani harness listing goes to backup, so it is one keystroke away if anyone pushes on how the proof is done. Deck is 31 talk slides now, down from 33 at the start of the day, on a 25-minute slot. 3. Slide 4 names the term. The claim was there but the word was not, so the audience had to supply the connection: what software-defined means down here is not features pushed over the air onto hardware chosen years ago, but software portable across silicon that stays verified across the move. The second half is the part almost nobody attempts, and it is what the rest of the deck is evidence for. Verified: zero clipped elements at 1024x768 and 1440x900, slide 21 on all four tabs, zero FSM mentions remaining in the talk path. Slide 4 reports a 10 px overflow at 4:3 that is bottom padding, not content -- its last line ends 108 px above the slide edge and 55 px above the nav, measured. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
It read "... and the FSM proves the absence", which continued slide 11's title before the merge and now stands alone -- with the one unexplained acronym in the deck. It is the slide you reach only when someone pushes on how the proof works, so it should read on its own: "The bounded proof behind that contract". Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…bundle
public/main.css begins with a U+FEFF BOM. read_text() keeps it, so the bundler
emitted "<style>:root{...}". A BOM is stripped when a stylesheet is FETCHED
with a charset; inside an inline <style> it is not, and ":root" is an invalid
selector -- so the browser dropped that entire first rule.
That first rule is the dark base palette. Consequences:
light mode fine, because the light overrides come later and parse
dark mode every custom property unset -- tokens rendered rgb(0,0,0), the
ground rgba(0,0,0,0). Black text on transparent.
Anyone opening the deck on a dark-mode machine got a broken page, and nothing in
the light-mode preview could reveal it. Found by testing both themes rather than
the one my browser happened to be in.
Fixed by stripping the BOM when inlining. Verified on the rebuilt bundle:
light tok-kw #7c3aed ground rgb(244,239,228) text rgb(26,34,53)
dark tok-kw #c084fc ground rgb(15,17,23) text rgb(225,228,237)
Both themes now define all six syntax colours and both grounds render.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
Slide 12 showed a verified own<dma-buffer> handoff and stopped there, which reads as a private seam. It is the embedded, verified instance of a general direction: shared-memory objects as a canonical-ABI option, where attach and detach ARE the ownership transfer. The alignment worth saying out loud is that the awkward case is our normal one -- the host answering zero and handing back a FIXED address, MPU rather than MMU, is exactly meld merged-memory plus synth --native-pointer-abi on an 8 KB part. That is a corner for most people and the default for us, which is the useful thing we can contribute to it. Grounded in FIND-DMA-SHM-CANONICAL-001 (artifacts/gust_dma_model.yaml), which records the design reference and that its author is aware of the work. Named the design reference rather than gesturing at "prior art", since half-credit was the reason an earlier slide got cut. Deliberately NOT included: a second attribution I could not ground. It appears in no artifact, doc or measurement in this repo, and the article offered as the source is by a different author and contains no substantive shared-memory content -- only a forward reference that shared-everything threads come after Component Model 1.0. Left out pending confirmation rather than asserted on a public slide. Slide 12 reports a 6 px overflow at 4:3 that is bottom padding, not content: its last line clears the nav by 59 px, measured. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
The outlook cited a design reference but not the question behind it. The framing question is Luke Wagner's "Does the Component Model Require Extra Copying?", and at 8 KB it is not academic -- a copy at the seam is a copy we cannot afford. So the slide now leads with the question and gives our answer: attach and detach ARE the transfer, not a hand-off plus a copy. The body says "a transfer, not a copy" explicitly, which is the thing the ledger's 220 B / 0 SRAM / 6 Kani proofs is evidence for. Both references named -- Luke Wagner for the question, Christof Petig's wasm-shm-test for the design. Recorded in gale as FIND-DMA-SHM-CANONICAL-001 (gale#256), checked against the sources rather than recalled. Slide 12 reports 19 px overflow at 4:3 that is bottom padding, not content: its last line clears the nav by 46 px, measured. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
The outlook was set at the .slide__cite default of 92ch, so it wrapped into a tall four-line column in the left two-thirds while the right third sat empty -- competing with the body block above it for the same measure, which is what made the slide feel crowded rather than full. Added .slide__cite.is-wide (max-width: 100%) and applied it. Width alone was not enough -- it went 837 -> 922 px at 4:3 and the height did not move, because the text still wrapped to four lines -- so the outlook and the body paragraph were both cut. body paragraph 119 -> 79 px outlook 157 -> 131 px slide 12 19 px over -> ZERO, clearing the nav by 65 px Zero overflow and zero clipped elements across all 38 slides at 1440x900, and only slide 4's known padding-only 10 px at 1024x768. The outlook spans 1296 px at 16:10. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…vered deck Two sections were doing one job, and one of them was half-built: talks/ was `render = false` and absent from the nav, so publishing the deck would have put it on the site reachable only by direct URL. Merged into content/publications/ -- "what we wrote for people". reports/ stays separate: it is what the TOOLS produced (rivet compliance, witness MC/DC), which is a different kind of artifact. Live URLs preserved by alias, verified in the built output: /preprints/oracle-gated-agent-loops/ -> /publications/oracle-gated-agent-loops/ /talks/wasm-research-day-2026/ -> /publications/wasm-research-day-2026/ The deck is published; the speaker notes are NOT -- draft = true, kept in the repo. Two bugs found on the way: 1. `aliases` landed after [taxonomies], so Zola read it as a taxonomy and the build failed outright. Moved above the block. 2. Worse, because it was silent: tools/bundle-talk.py still pointed at the OLD slug, which now resolves to the alias REDIRECT STUB. It happily produced a 483 B file -- fonts inlined, exit 0, "success" -- and would have overwritten the 652 KB deck with a redirect page. Fixed the slug and added a guard that refuses to write when the source has no slides. Verified the guard fires on the stale path. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Draft on purpose. Per the standing instruction this is committed and pushed but not merged — merging to
maintriggersdeploy.ymland publishes to the site. Opening it as a draft getsci.ymlto exercise the build for the first time without any risk of an accidental merge.The talk is today. The presentation artifact is the self-contained bundle, not this branch.
What it is
33 talk slides + 4 backup, for a 25-minute slot + 5 min Q&A. 48 commits.
Verified standalone (not just "it builds")
Served from a directory containing nothing but the single file:
src/hrefrefsfetch()calls that would firefetchis behindwindow.__CASTS, and the cast is inlinedXMLHttpRequest/Worker/WebSocket?fresh=1#34lands on 34/37, the right backup slide ✓file://)The reload-resume path matters for a remote talk: if the call drops or the browser reloads, the deck comes back on the slide you were on rather than the title.
Q&A navigation
Hash is read on load but there's no
hashchangelistener, so typing#34into the URL bar mid-talk won't jump. The working path to backup slides is the overview (grid button / key), then click the slide. That is tested and works.Backup slides
Companion page
content/talks/wasm-research-day-2026-notes.md— every number in the deck: what it measures, what it does not mean, its source, and the corrections made while building it (the USART 326→254 B figure, the spi 1244→1450 B figure, the 11→5 linear-memory miscount, and the falsified "a compiler with no verifier cannot reach it" claim).Not for merge today
Merging publishes. Leaving as draft.