Whitepaper v2 Section 8: Future Work & Roadmap (~2,900 words)
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 1s
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 1s
Completes the whitepaper. Covers: - 8.1 Compiler completeness (record types, action bodies, in operator, Map ops, host binding, TigerBeetle E2E) - 8.2 Language extensions (temporal properties, function types, modules, parametric types) - 8.3 Tooling ecosystem (LSP, IDE plugins, package registry, CI/CD) - 8.4 Strategic roadmap (Open Standard → Consulting → SaaS → Compliance API) - 8.5 What Will Not Change (small language, mandatory provenance, MIT, evidence over proof) - Conclusion: the case for accountable software All 8 sections complete. ~19,000 words total.
This commit is contained in:
Scott Scoble
parent
940b959efb
commit
6121fd6a8f
1 changed files with 201 additions and 2 deletions
|
|
@ -1207,8 +1207,207 @@ TLA+ proves your algorithm works. Coq proves your implementation matches your sp
|
|||
|
||||
## 8. Future Work and Roadmap
|
||||
|
||||
*[Section 8: Record types, temporal properties, IDE integration, ecosystem]*
|
||||
This whitepaper has described a specification language (SpeckDL), a compiler that transforms specifications into runnable code, and a provenance system that turns every compilation into auditable evidence. The toolchain is functional today — it parses, compiles, and generates. But a working prototype and a mature ecosystem are different things. This section maps what exists, what is actively under construction, and what must still be built.
|
||||
|
||||
### 8.1 Compiler Completeness (Active, May 2026)
|
||||
|
||||
The Speckl compiler currently produces three primary artifacts from a valid `.speckdl` file: a TypeScript module, a WebAssembly Text (WAT) module, and three supply-chain provenance documents (PROV-O, CycloneDX, SPDX). This is a non-trivial baseline, but it is not complete. The following gaps are either being worked on now or are the next queued items.
|
||||
|
||||
#### Record Types in Generated Code
|
||||
|
||||
The parser already recognizes `record` declarations. The type checker enforces field access. But the TypeScript and WASM generators do not yet emit record constructors or field access code. This means a spec that declares `record Transfer { from: AccountId; to: AccountId; amount: Balance }` will parse correctly but the generated code will reference a type that does not exist in the output. This is the single largest blocker for complex specs (the naive TigerBeetle port, for example, is held up by missing record emission).
|
||||
|
||||
Fixing this requires:
|
||||
1. **TypeScript generator:** Emit interface or class declarations for each `record` in the spec.
|
||||
2. **WASM generator:** Implement host-side record boxing (struct values that cross the host/wasm boundary as opaque handles rather than flat tuples).
|
||||
3. **Validation:** The TigerBeetle spec and the compiler self-spec both have 20+ TypeScript errors, roughly half of which are missing record types.
|
||||
|
||||
#### Parser: Action Bodies
|
||||
|
||||
The parser supports `action` declarations with preconditions and postconditions, but action bodies — the `require`, `assign`, `emit`, and `return` statements that define *how* the state changes — are currently parsed into the AST but not fully validated during compilation. The compiler generates guard functions but leaves action implementations stubbed or empty. This is a known parser issue (tracked in `engineering#9`) and is the next parser fix after record types.
|
||||
|
||||
#### The `in` Operator
|
||||
|
||||
Set membership tests (`x in S`) parse correctly, but the WASM code generator does not yet emit `i32` search loops for linear collections or bit tests for small fixed sets. The TypeScript generator handles `in` correctly because it can delegate to native `Array.includes` or `Set.has`. The WASM path is the remaining work.
|
||||
|
||||
#### `Map<K,V>` Operations
|
||||
|
||||
`Map<K,V>` declarations parse and type-check. TypeScript generation delegates to native `Map`. WASM generation requires a hash-table or linear-search implementation in the generated WAT. Not yet implemented.
|
||||
|
||||
#### Host-Side Binding for WASM
|
||||
|
||||
The WASM module exports `init`, `getState`, and individual `action` functions. But there is no lightweight JavaScript wrapper that handles:
|
||||
- Converting JavaScript strings/numbers into the WASM memory layout
|
||||
- Calling an action, reading the updated state, and converting back
|
||||
- Error handling when a guard rejects an action
|
||||
|
||||
This wrapper is ~150 lines of boilerplate but is required for any real deployment. Until it exists, WASM artifacts are "valid but not usable from JavaScript."
|
||||
|
||||
#### `wat2wasm` End-to-End for TigerBeetle
|
||||
|
||||
The Counter spec compiles through `wabt` (parse + resolve + validate + binary) and runs in Node.js with confirmed state mutations. The TigerBeetle spec validates through `wabt` but has not yet been assembled to binary and executed end-to-end. The blocker is the record type issue described above; once records emit correctly, the TigerBeetle E2E test is the natural next validation step.
|
||||
|
||||
### 8.2 Language Extensions (Planned)
|
||||
|
||||
Beyond compiler completeness, several language features are planned but not yet designed or implemented.
|
||||
|
||||
#### Temporal Properties (`always`, `eventually`, `leadsTo`)
|
||||
|
||||
TLA+ and other temporal logics distinguish between *safety* properties ("bad things never happen") and *liveness* properties ("good things eventually happen"). SpeckDL currently expresses only safety (through `precondition` and `postcondition` guards). The next major language extension is temporal property syntax:
|
||||
|
||||
```speckdl
|
||||
temporal {
|
||||
always( Balance >= 0 )
|
||||
eventually( TransferConfirmed )
|
||||
leadsTo( TransferInitiated, TransferConfirmed )
|
||||
}
|
||||
```
|
||||
|
||||
These properties would not be checked at runtime (that would require a model checker or proof assistant). Instead, they would be:
|
||||
- **Emitted as documentation** in the provenance artifacts, so auditors know the intended liveness guarantees.
|
||||
- **Checked during compilation** where possible (e.g., a simple `always` property can sometimes be proven by static analysis of the state machine).
|
||||
- **Exported as test targets** for external model checkers (e.g., generate a TLA+ snippet from the temporal property for teams that already use TLC).
|
||||
|
||||
This is the bridge between "specs for runtime" and "specs for proof."
|
||||
|
||||
#### Function Types and Higher-Order Actions
|
||||
|
||||
Currently, actions are flat: they take scalar and collection inputs and mutate state. There is no support for:
|
||||
- Passing an action as a parameter to another action
|
||||
- Function composition or pipeline syntax
|
||||
- User-defined helper functions
|
||||
|
||||
The syntax is reserved (`fn` keyword is not yet allocated) but the type system will need significant extension to support function types without compromising the state-machine compilation model.
|
||||
|
||||
#### Module System and Imports
|
||||
|
||||
Real specifications are not monolithic. A banking ledger should import a `currency` module. A consensus protocol should import a `network` module. The module system is not yet designed, but the grammar has reserved `import` and `module` keywords. The planned design:
|
||||
- **Static imports** at parse time (no dynamic loading)
|
||||
- **Namespace-qualified names** (`network.SendMessage`)
|
||||
- **Re-export** for provenance chains (if module A imports module B, the provenance graph includes B's compilation hash)
|
||||
|
||||
#### Parametric Types
|
||||
|
||||
`List<T>`, `Set<T>`, and `Map<K,V>` are the only generic types today. Full parametric types (user-defined `Stack<T>`, `Queue<T>`, `Result<T,E>`) require template instantiation in the generators and are deferred until the module system is stable.
|
||||
|
||||
### 8.3 Tooling and Ecosystem
|
||||
|
||||
A language without tooling is a specification without users. The following ecosystem components are planned:
|
||||
|
||||
#### Language Server Protocol (LSP) Integration
|
||||
|
||||
The parser is fast enough for real-time feedback (~50ms for a 500-line spec). An LSP server would provide:
|
||||
- Syntax highlighting (tree-sitter grammar, already drafted)
|
||||
- Error squiggles at edit time
|
||||
- "Go to definition" for state variables and action names
|
||||
- Hover types for expressions
|
||||
- Auto-completion for keywords and built-in types
|
||||
|
||||
The TypeScript generator already produces clean `.ts` files that `tsc --noEmit` validates, so an LSP could also surface TypeScript-level errors inside the spec editor.
|
||||
|
||||
#### IDE Plugins
|
||||
|
||||
LSP integration enables VS Code, Vim, Emacs, and Zed support with minimal per-editor work. A dedicated VS Code extension would add:
|
||||
- A "Compile" button that runs `speckl-compile` and shows all 5 output artifacts
|
||||
- A side-panel provenance viewer (rendering PROV-O as a human-readable trace)
|
||||
- One-click deployment to Storj, Cloudflare Pages, or self-hosted static hosting
|
||||
|
||||
#### Package Registry
|
||||
|
||||
The module system will need a package registry for reusable specifications:
|
||||
- `speckl install consensus/raft` — imports the Raft consensus spec from a central registry
|
||||
- Each package version includes its own provenance chain
|
||||
- Packages can be pinned by content hash (immutable, auditable)
|
||||
|
||||
The registry would be a static site (Speckl packages are plain text) hosted on Storj or IPFS, with a simple CLI for publish/install.
|
||||
|
||||
#### CI/CD Integration
|
||||
|
||||
The long-term vision is a `speckl-validate` GitHub Action / Forgejo Action that:
|
||||
- Runs on every PR
|
||||
- Recompiles all `.speckdl` files
|
||||
- Checks that generated artifacts match committed versions (no drift)
|
||||
- Verifies provenance signatures
|
||||
- Fails the build if a spec compiles to code with TypeScript errors or WASM validation failures
|
||||
|
||||
This turns "specs as documentation" into "specs as build gate."
|
||||
|
||||
### 8.4 Strategic Roadmap
|
||||
|
||||
Speckl's development follows a strategy ladder — not a single product, but a sequence of products that build on the same core technology.
|
||||
|
||||
#### Phase 1: Open Standard (Now — Summer 2026)
|
||||
|
||||
**Goal:** Establish credibility, attract early adopters, build a community of specification authors.
|
||||
|
||||
- Complete compiler (record types, action bodies, `in` operator, Map ops)
|
||||
- Publish whitepaper v2 (this document)
|
||||
- Submit to academic venues (workshops on formal methods, software engineering, supply chain security)
|
||||
- Release "Speckl by Example" tutorial and consensus protocol specs as reference implementations
|
||||
- Publish on Show HN, Lobsters, and relevant subreddits
|
||||
- Seek 3-5 design partners (companies with compliance requirements willing to pilot Speckl)
|
||||
|
||||
**Success metric:** 100+ GitHub/Codeberg stars, 3 design partners, 1 conference talk accepted.
|
||||
|
||||
#### Phase 2: Consulting (Summer — Fall 2026)
|
||||
|
||||
**Goal:** Generate revenue while refining the product through real client use.
|
||||
|
||||
- Offer "Speckl adoption consulting" — help teams write their first specs, integrate the compiler into their CI pipeline, and train engineers on the language
|
||||
- Pricing: $5,000–$15,000 per engagement (2-4 weeks of part-time work)
|
||||
- Use consulting engagements to discover the most painful gaps in the toolchain
|
||||
- Publish case studies (with client permission) as proof of production use
|
||||
|
||||
**Success metric:** 3 consulting engagements, $15,000+ revenue, 2 published case studies.
|
||||
|
||||
#### Phase 3: Developer Tool / SaaS (Fall 2026 — 2027)
|
||||
|
||||
**Goal:** Productize the consulting learnings into a self-serve tool.
|
||||
|
||||
- Web-based IDE (or VS Code extension with cloud backend)
|
||||
- Hosted compiler API (upload `.speckdl`, receive all 5 artifacts)
|
||||
- Team collaboration features (shared specs, review workflow, versioned provenance)
|
||||
- Freemium pricing: free for open-source specs, paid for private specs and CI integration
|
||||
|
||||
**Success metric:** 50+ paying teams, $2,000+ MRR.
|
||||
|
||||
#### Phase 4: Compliance API (2027+)
|
||||
|
||||
**Goal:** Deep integration into enterprise compliance and audit workflows.
|
||||
|
||||
- SOC 2 / ISO 27001 / NIST 800-53 mapping (each control mapped to SpeckDL specs that demonstrate compliance)
|
||||
- API for audit tools (read provenance, verify signatures, generate audit reports)
|
||||
- Integration with SBOM platforms (Syft, Anchore, SLSA attestations)
|
||||
- Enterprise pricing: $500+/month per team
|
||||
|
||||
**Success metric:** 5+ enterprise customers, $10,000+ MRR.
|
||||
|
||||
### 8.5 What Will Not Change
|
||||
|
||||
The roadmap is ambitious, but several core decisions are fixed:
|
||||
|
||||
1. **SpeckDL stays small.** The language will not grow into a general-purpose programming language. If you need loops, recursion, or I/O, you are outside SpeckDL's domain. Use TypeScript or Rust for that, and use SpeckDL for the parts that must be provable.
|
||||
|
||||
2. **Provenance is not optional.** Every compiler version, every spec, every generated artifact will always have a verifiable provenance chain. This is not a premium feature; it is the foundation.
|
||||
|
||||
3. **Open source, MIT license.** The compiler, the language specification, and the reference implementations will remain open source. Revenue comes from tooling, consulting, and hosted services — not from license fees.
|
||||
|
||||
4. **Evidence over proof.** SpeckDL will not become a theorem prover. It will remain the language for teams that need *evidence* of correctness (runtime guards, provenance chains, audit trails) rather than *proof* of correctness (formal verification, model checking). Teams that need proofs should use TLA+, Coq, or Dafny — and they can import SpeckDL specs into those tools where overlap exists.
|
||||
|
||||
---
|
||||
|
||||
*Whitepaper v2 draft. Sections 1-6 complete; 7-8 forthcoming.*
|
||||
## Conclusion
|
||||
|
||||
Software engineering has spent decades building tools that make code *faster* to write. We have spent far less time building tools that make code *accountable* to the people who depend on it. Speckl is a bet that the next shift in software quality will not come from faster type checkers or better linters, but from systems that can answer the question: *"How do you know this code does what the specification says?"*
|
||||
|
||||
The answer Speckl proposes is simple: make the specification executable, make the compilation traceable, and make the evidence permanent. A spec that compiles to runnable code with compiler-generated provenance is not a wish list — it is a contract with a receipt.
|
||||
|
||||
The toolchain is young. The language is small. The community is just starting. But the foundation is solid: a specification language that compiles to both TypeScript and WebAssembly, with built-in supply chain provenance, tested against consensus protocols that have been formally verified elsewhere, and designed for the specific gap between "we wrote a spec" and "we can prove we followed it."
|
||||
|
||||
If you build systems that matter — systems where a bug means a compliance fine, a safety incident, or a loss of trust — consider writing your next specification in SpeckDL. The compiler will tell you if it is valid. The provenance will tell you if it was followed. And the generated code will tell you if it still runs.
|
||||
|
||||
**Start at:** [speckl.scoble.me](https://speckl.scoble.me)
|
||||
|
||||
**Source code:** [os.scoble.me/forgejo/sscoble/speckl](https://os.scoble.me/forgejo/sscoble/speckl)
|
||||
|
||||
**Whitepaper v2 complete. All 8 sections shipped. May 7, 2026.**
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue