Sean Allen, a software engineer on the Red Team at Antithesis, discusses his journey from music to programming, the design of programming languages that prevent bugs by construction, and a philosophy of software correctness that prioritizes static verification over late-stage testing.
Background and path into programming
Allen graduated with no clear direction, moved to New York City, and got a job fixing computers at Scholastic before a friend suggested learning Perl to join a startup in Boston.
The startup collapsed, but he discovered he enjoyed programming and could earn well doing it; his first exposure was a Commodore 64 machine-language book his grandmother bought, which made programming seem impossibly hard.
He invested heavily in self-study, gravitating toward BeOS and C++; the head of compiler tools at Metrowerks and sci-fi author Neal Stephenson (then active on mailing lists) mentored him in C++.
He later chose C and Ada as his two focus languages: C for Mac OS development, Ada for its rigorous static checking aimed at mission-critical systems (defense, NASA).
Ada’s strictness frustrated him — his programs wouldn’t compile — while C programs compiled but segfaulted; years later he realized he’d rather have the compiler enforce the rules he’d painstakingly developed for safe C/C++ concurrency.
Antithesis and the Red Team
Will Wilson (CEO) recruited Allen via a “Who’s Hiring” post; the role was essentially “do Jepsen-style things” — i.e., fault-injection testing of distributed systems.
The Red Team uses the product exactly as customers do, with no internal tooling privileges, to surface usability gaps and teach both customers and colleagues how to build reliable software.
Allen’s focus is on correctness techniques that start “way down the stack,” long before anything called testing.
Programming languages that enforce correctness by construction
OCaml: descended from ML; combines functional programming with object-oriented features (the “O”), though almost no production OCaml code uses the O features. Its sum types, pattern matching, and exhaustive matching let the compiler flag every unhandled case when a type changes — a “gloriously wonderful experience.”
F#: Microsoft Research’s “OCaml for .NET,” created by Don Syme. Its distinction is seamless .NET interop without the rough edges common on the JVM (e.g., Scala/Java). F# and .NET co-evolved symbiotically; many F# features later migrated to C#, with exhaustive matching on sum types the main remaining gap.
Pony: open-source, actor-model language co-created by Allen’s college friend Sylvan Clebsch (PhD at Imperial College). Designed for fast, highly asynchronous, concurrent programs with compiler-enforced memory safety — “fearless concurrency” baked in, not assembled from libraries.
Each actor has its own heap; garbage collection runs per-actor between work units, eliminating stop-the-world pauses and yielding flat tail latencies (trade-off: slightly lower peak throughput).
The type system makes illegal states unrepresentable, similar to Rust but with a built-in actor model that simplifies reasoning about concurrency.
Ada: still used in high-assurance domains; its selling point against Rust is “more guarantees.”
Rust: heavily ML-influenced (sum types, pattern matching); provides strong static guarantees but lacks a built-in concurrency model — you compose your own.
Software correctness: testing as a means, not an end
Allen defines correctness as “my program does what I expected it to do” — upholding invariants, not waking anyone at 2 a.m.
Tests are a means to an end; the end is correctness. Testing happens late; better to encode invariants in the type system (sum types, exhaustive matching, legal state transitions) so the compiler prevents whole classes of bugs before tests run.
TDD is excellent for API design, but example-based tests can be defeated by hard-coded implementations; property-based testing (randomized inputs) forces genuine correctness.
Workloads: the combination of system under test, validation logic, and input generation that drives interesting behavior. A naive “drunken walk” of random operations rarely hits edge cases (e.g., 10,000 puts in a row triggering resharding).
Bank test: simple workload for isolation guarantees — transfer money between accounts in transactions while a concurrent reader checks the total never deviates from $10,000. Under fault injection (network partitions, node kills), subtle bugs surface.
Workloads are not scripted scenarios; they define rules and let the generator explore.
Quality is not a gate
The “gate” metaphor assumes quality is kept by catching bad things at the door. In reality, every layer (code review, CI, staging, observability) has holes; production is always the final test.
High-functioning teams build correctness in from the start: formal specs (TLA+, Alloy), strong type systems, early fault-injection testing (Jepsen/Antithesis) on the first version, and designing for observability.
Low-functioning teams rely on late gates (PR checks, staging) and move slowly or ship bugs.
Business logic can be statically constrained (e.g., state machines in the type system), though no language eliminates all need for testing — performance and ecosystem trade-offs force compromises.
Supply chain security
Attack the weakest link: compromise a popular dependency (e.g., left-pad on npm, malicious PyPI packages) to inject code that runs with the same privileges as the application.
Naive defenses (cool-down periods, vendoring, forking) fail: cool-downs delay security fixes; vendoring/forking doesn’t scale; someone must still audit the code.
Root cause: almost every language’s package model (inherited from CPAN) assumes a trusting, good-actor ecosystem. Code from the internet has full ambient authority (network, filesystem, crypto miners).
Object capabilities (e.g., language E, and built into Pony) require explicit capabilities for any side effect (network, FS); the host program delegates only what’s needed. But FFI (C/Rust interop) bypasses this unless also capability-controlled.
Confidential computing (encrypted VMs, attestation) protects data from cloud operators, but speculative execution side channels (Spectre/Meltdown family) break all guarantees; mitigations cost 50%+ performance, so the industry plays whack-a-mole rather than disable speculation.
Technical debt: not all debt must be repaid
“Technical debt only hurts if you have to pay it back.” Teams often sidestep debt: throw money at a managed service (e.g., distributed SQL), delete the system when the business pivots, or never hit the scaling limit.
Debt becomes a trap only when it prevents necessary changes before product-market fit.
The “all debt is bad” dogma doesn’t match reality; successful companies pay debt because they succeeded, not because debt is inherently fatal.
Go slow to go fast
Counterintuitive practices that accelerate delivery:
Write a planning doc and agree on scope before coding.
Define how to test/observe the system before building.
Spike unknowns for a few hours/days.
Stop and fix when production is on fire at 2 a.m. (rested brains make fewer mistakes).
Align vocabulary: weeks of misaligned work stem from never defining terms (e.g., “exactly once” meaning delivery vs. processing).
Design for observability and testability up front — gray failures (bad UX, healthy load balancer) are invisible without deliberate instrumentation.
