Onward! 2025
2025-10-12..2025-10-18
Singapore, Singapore
Onward! ·
[Onward! 2020, Onward! 2021, Onward! 2022, Onward! 2023, Onward! 2024, Onward! 2025]
who it's for
language designers, software architects, program verification engineers, developer experience engineers, tooling and IDE engineers, documentation engineers, computational chemistry software engineers
topics
filesystem as object store; binary and high-level proofs; minimal verified components; GenAI-native software stacks; peptide chemistry DSL; grammar to LL(1) transformation; programmable typography runtimes; execution-derived documentation; nested example program synthesis; probabilistic program self-inference; energy-aware by-construction refinement; synchronous game programming model
| title | author | length |
|---|---|---|
| The Unix Executable as a Smalltalk Method | Joel Jakubovic | 51m |
Argues the concrete claim Unix executable = Smalltalk method and shows a proof‑of‑concept: Squeak crossmorph methods hand‑compiled into bash‑compiled methods… | ||
| The Proof Must Go On: Formal Methods in the Theater of Secure Software Development(…) | Charles Averill | 48m |
Predicts full-stack proof frontends within a decade that combine binary and high-level proofs, and widespread minimal verified components that become pluggable… | ||
| Foundational Design Principles and Patterns for Building Robust & Adaptive(…) | Frederik Vandeputte | 36m |
Argues future systems embed GenAI but design for probabilistic outputs by adding runtime checks, metadata and feedback loops, plus mechanisms to convert slow… | ||
| TideScript: A Domain Specific Language for Peptide Chemistry | Nicholas Morris, Blair Archibald, S Hessam M Mehr | 30m |
TideScript is a domain-specific language with a formal syntax and small-step operational semantics that encodes SPPS chain assembly, peptide cleavage, and… | ||
| Semantics-preserving Transformation of Context-free Grammars into LL(1) Form | Vladyslav Bilyk | 31m |
Proposes a concrete method to convert any context-free grammar into LL(1) while keeping the original semantics by encoding rules as typed tree nodes and… | ||
| Carving Text at Its Joints: A New Perspective on Writing and Computers | Kevin Graaf | 39m |
Argues that much script complexity is extrinsic and fixes come from new abstractions: a concrete Teleode encoding (ordered labeled entry trees, base characters… | ||
| Literate Tracing | Matthew Sotoudeh | 31m |
Argues that documentation built from annotated, concrete executions makes huge codebases understandable: literate traces walk real runs, show input→output, and… | ||
| ScooPy: Enhancing Program Synthesis with Nested Example Specifications | Tomer Katz, Hila Peleg | 28m |
ScooPy integrates an IDE synthesizer with example scopes — comment-wrapped input/output examples that can be edited, live-checked, nested, and re-used to… | ||
| What You See Is What It Does: A Structural Pattern for Legible Software | Eagon Meng, Daniel Jackson | 28m |
Claims a concrete structure called concepts and synchronizations that separates concerns into independent services and declarative event rules, implements a… | ||
| Gauguin, Descartes, Bayes: A Diurnal Golem's Brain | Kartik Chandra, Amanda Liu, Jonathan Ragan-Kelley, Joshua B. Tenenbaum | 39m |
Builds a small probabilistic program in Church that samples and conditions over program-space to infer its own source; uses a grammar-based generator, eval… | ||
| X-by-Construction: Towards Ensuring Non-Functional Properties in by-Construction(…) | Maximilian Kodetzki, Tabea Bordis, Alex Potanin, Ina Schaefer | 28m |
Proposes generalizing X-by-Construction to non-functional properties, defines six concrete requirements for a property to fit into by-construction workflows… | ||
| Synchronous Programming for Kids: A Manifesto | Jean Pichon-Pharabod | 42m |
Argues that primary‑school game programming fits a synchronous model better than Scratch’s imperative handlers and shows a working prototype called Reactive… | ||
| Let's Take Esoteric Programming Languages Seriously | Jeremy Singer, Steve Draper | 40m |
Claims that esoteric languages boost programmer awareness and teach language design through constraint and surprise, backed by concrete examples: Whitespace… | ||
| Exploring The Design Space For Runtime Enforcement of Dynamic Capabilities | Andrew Fawcett, James Noble, Michael Homer | 32m |
Dala implements three safe object flavours—ISO (isolated), immutable, local—and the paper enumerates six enforcement axes that yield 2,880 combinations and… | ||
| nothing matches | ||