whitepaper v2: Section 1 (The Spec-Code Gap) with executable specs framing
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 3s
Some checks failed
Deploy Landing Page to Storj / deploy (push) Failing after 3s
Rewrites the whitepaper from the old 'Dark Provenance' concept to reflect what Speckl actually is now: specifications that compile to software. Section 1 covers: - The Archaeology Problem (specs that rot in docs) - The Formal Methods Gap (verified spec ≠ running system) - The SpeckDL Approach (compile spec directly to code + provenance) - Concrete ToggleSwitch example (14 lines → 5 artifacts) Whitepaper outline restructured around current compiler capabilities (TypeScript, WASM, PROV-O, CycloneDX, SPDX generators).
This commit is contained in:
Scott Scoble
parent
d03b5b41a6
commit
2ed6c13026
1 changed files with 104 additions and 0 deletions
104
docs/whitepaper-v2.md
Normal file
104
docs/whitepaper-v2.md
Normal file
|
|
@ -0,0 +1,104 @@
|
|||
# Speckl: Closing the Spec-Code Gap with Compilable Specifications
|
||||
|
||||
> *A whitepaper on SpeckDL, a domain-specific language for writing specifications that compile to runnable software with embedded provenance.*
|
||||
|
||||
## Abstract
|
||||
|
||||
Software specifications have a fundamental problem: they describe what code should do, but they cannot guarantee what code actually does. Formal methods (TLA+, Alloy, Coq) can verify properties of specifications, but their outputs remain disconnected from production systems — the spec and the code evolve independently until the spec becomes archaeology.
|
||||
|
||||
Speckl introduces a different approach: **specifications that compile to software**. The SpeckDL language lets you write state machine specifications with types, invariants, and actions — then compiles them into five auditable artifacts: PROV-O provenance graphs, CycloneDX SBOMs, SPDX license documents, TypeScript classes, and WebAssembly modules. The spec isn't documentation alongside the code — the spec IS the code, with a verifiable chain from intent to implementation.
|
||||
|
||||
This paper presents the SpeckDL language, its compiler architecture, and the provenance model that makes every generated artifact auditable back to its specification. We demonstrate SpeckDL on consensus protocols (Two-Phase Commit, Paxos, Raft) and a financial ledger, showing how the same specification produces both formal verification artifacts and production-runnable modules.
|
||||
|
||||
## 1. The Spec-Code Gap
|
||||
|
||||
Every software project has specifications. Requirements documents, architecture decision records, API contracts, RFCs — these artifacts describe intent. But they have a fatal flaw: **they cannot be executed, and therefore cannot be verified against reality.**
|
||||
|
||||
### 1.1 The Archaeology Problem
|
||||
|
||||
When a specification exists only as prose, it decays. Three months after writing, the spec describes what the system should have done, not what it does now. Engineers treat specs as orientation, not authority. The spec becomes archaeology — interesting for historical context, irrelevant for current behavior.
|
||||
|
||||
This decay compounds with AI-generated code. When an LLM writes code from a prompt, the reasoning chain is opaque. The generated code may satisfy the prompt, violate it in subtle ways, or introduce behaviors the prompt never specified. Without an executable connection between intent and output, verification is reduced to testing — which can only prove the presence of bugs, not their absence.
|
||||
|
||||
### 1.2 The Formal Methods Gap
|
||||
|
||||
Formal specification languages (TLA+, Alloy, Isabelle/HOL) solve the precision problem: they express intent unambiguously and can model-check properties of that intent. TLA+ in particular has been used to find critical design bugs in systems at AWS, Microsoft, and MongoDB.
|
||||
|
||||
But formal methods create their own gap: **the verified spec and the running system are separate artifacts.** After model-checking a TLA+ specification, someone must manually translate it into a programming language. That translation introduces the same spec-code gap the formal method was supposed to close. The implementation can diverge from the verified spec, and no tool detects it.
|
||||
|
||||
### 1.3 The SpeckDL Approach
|
||||
|
||||
SpeckDL sits between prose specifications and formal methods. It provides:
|
||||
|
||||
1. **Executable semantics:** Specifications compile to runnable code (TypeScript classes, WebAssembly modules). The spec doesn't describe the system — the spec IS the system, compiled directly.
|
||||
2. **Verifiable invariants:** State invariants are checked at runtime through guard statements (`require`), providing living verification rather than one-time model checking.
|
||||
3. **Embedded provenance:** Every compilation produces a PROV-O graph tracing each output artifact back to the specification elements that generated it. You can answer "why does this code exist?" by following the provenance chain.
|
||||
4. **Supply chain transparency:** The compiler emits CycloneDX SBOMs and SPDX documents automatically, making AI-generated code auditable for compliance frameworks (NIST SA-11, SOC 2, FedRAMP).
|
||||
|
||||
### 1.4 A Concrete Example
|
||||
|
||||
Consider a ToggleSwitch specification in SpeckDL:
|
||||
|
||||
```
|
||||
state ToggleSwitch {
|
||||
on: Bool
|
||||
}
|
||||
|
||||
init ToggleSwitch {
|
||||
on = false
|
||||
}
|
||||
|
||||
action TurnOn for ToggleSwitch {
|
||||
on = true
|
||||
}
|
||||
|
||||
action TurnOff for ToggleSwitch {
|
||||
on = false
|
||||
}
|
||||
|
||||
invariant NoDoubleToggle for ToggleSwitch {
|
||||
require TurnOn => !on // Can't turn on if already on
|
||||
require TurnOff => on // Can't turn off if already off
|
||||
}
|
||||
```
|
||||
|
||||
From these 14 lines, `speckl compile` produces:
|
||||
- **TypeScript:** A `ToggleSwitch` class with typed `TurnOn()` and `TurnOff()` methods, guard checks, and state accessors
|
||||
- **WebAssembly:** A `.wasm` module with exported `turn_on` and `turn_off` functions with guard-validated state transitions
|
||||
- **PROV-O:** A provenance graph showing that the `TurnOn` method was derived from the `action TurnOn` spec block
|
||||
- **CycloneDX:** An SBOM declaring the generated module with its hash and provenance
|
||||
- **SPDX:** A license document for the generated artifact
|
||||
|
||||
The specification is 14 lines. The generated artifacts are hundreds of lines of production code. The provenance chain connects every line back to the 14-line intent. This is the spec-code gap, closed.
|
||||
|
||||
## 2. The SpeckDL Language
|
||||
|
||||
*[Section 2: Full language specification — types, state machines, actions, invariants, compilation targets]*
|
||||
|
||||
## 3. Compiler Architecture
|
||||
|
||||
*[Section 3: Parser → AST → Generators pipeline, multi-target compilation, test infrastructure]*
|
||||
|
||||
## 4. Embedded Provenance
|
||||
|
||||
*[Section 4: PROV-O generation, provenance graph structure, audit trail semantics]*
|
||||
|
||||
## 5. Consensus Protocols in SpeckDL
|
||||
|
||||
*[Section 5: Two-Phase Commit, Paxos, and Raft case studies with compilation results]*
|
||||
|
||||
## 6. Compliance and Supply Chain
|
||||
|
||||
*[Section 6: NIST SA-11 alignment, SBOM automation, regulatory use cases]*
|
||||
|
||||
## 7. Related Work
|
||||
|
||||
*[Section 7: Comparison with TLA+, Alloy, Coq, Dafny, and code generation approaches]*
|
||||
|
||||
## 8. Future Work and Roadmap
|
||||
|
||||
*[Section 8: Record types, temporal properties, IDE integration, ecosystem]*
|
||||
|
||||
---
|
||||
|
||||
*Whitepaper v2 draft. Sections 1 complete; 2-8 forthcoming.*
|
||||
Loading…
Add table
Add a link
Reference in a new issue