▶ YouTube Summaries

• YT :: https://www.youtube.com/watch?v=OrXKvOjR-vI
• Original title :: Software correctness and programming languages with Sean Allen

Gergely interviews Sean Allen (Distinguished Engineer at Antithesis, maintainer of the Pony language) about fundamentals of building correct software, deliberately avoiding the topic of AI. Themes: ML-family languages (OCaml, F#), Ada and Pony as compiler-enforced correctness, per-actor garbage collection, why tests are a means and not the goal, property-based testing and "workloads", why quality is not a gate, supply chain security and object capabilities, side-channel attacks and confidential computing, a revised view of technical debt, and planning up front as the way to go fast.

Path into tech and Antithesis

• Started in music; after college landed in New York fixing computers at Scholastic, then learned Perl (on a friend's tip) for a Boston startup that collapsed before he started.
• First programming book was a Commodore 64 machine-language book, picked by a grandmother who knew nothing about programming; motivated by the game Lode Runner.
• Learned C++ on the BeOS mailing lists, helped by the head of the Metrowerks compiler group and by Neal Stephenson (unknown to him at the time as a sci-fi author).
• Joined Antithesis after the CEO Will Wilson sent a Hacker News "who is hiring" link ("do you want to do Jepsen-style things?").
• Works on the Red Team: uses the product exactly as customers would, deliberately without internal tools; builds agent skills for working with Antithesis and teaches customers how to be sure that software works, starting "way down the stack, way before anything that anybody calls testing".

OCaml, ML family and exhaustive matching

• OCaml came from French academia, designed to combine functional and object-oriented programming; the object features are practically unused in the variant popular at Jane Street and similar firms.
• ML family (OCaml, F#, partly Haskell) is a separate lineage from the Algol family (Python, Perl, Ruby, C, C++). Rust is the best-known ML-influenced language: sum types and pattern matching.
• Sum types plus exhaustive pattern matching: adding a sixth variant to a type with five makes the compiler list every place that does not handle it. Validation is front-loaded to compile time.
• Type systems can encode the allowed states and transitions of a system, so illegal transitions cannot be expressed; reasoning about the system then only concerns what the type system does not already forbid.

Ada, C and the cost of a lenient compiler

• Chose C and Ada early in his career. Ada (defense, NASA, mission-critical) is deeply specified and refuses to compile incorrect programs; Ada vendors today pitch "you like Rust, how about more guarantees".
• Regret: could not get Ada programs to compile and took C compiling as "the cookie", ignoring that the C programs segfaulted constantly. Years went into building personal rules for writing concurrent C and C++ that avoid crashes, and humans still break such rules; a compiler should enforce them instead.

F# and .NET

• F# came out of Microsoft Research (Don Syme), starting as "OCaml for .NET".
• Its standout trait is not any single language feature but seamless fit with the .NET platform, unlike the rough edges of Scala on the JVM.
• F# evolved deliberately slowly, letting the .NET runtime catch up; features then flowed back into C#. The main thing still missing in C# is sum types with exhaustive matching, which seem likely to arrive.
• Side note: .NET and C# exist partly because of the Sun lawsuit over Microsoft's Windows-specific Java.

Pony and the actor model

• Pony is an open-source language created by a college friend (Sylvan Clebsch) after he built an actor-model runtime in C at Morgan Stanley and then did a PhD at Imperial on type systems.
• Sean needed a fast, concurrent, low-latency system for banks at Wallaroo (high-speed data processing); JVM stop-the-world garbage collection was unacceptable (Azul's pauseless JVM was too expensive), and C/C++ could not offer the guarantees with hireable people.
• Pony descends from the ML family and is aimed at fast, highly asynchronous concurrent programs where the compiler enforces the rules that keep programs from crashing; the actor model is built in, as in Erlang/Elixir, and object capabilities are built in too.
• Positioning: fearless concurrency as one coherent package, instead of picking and combining pieces as in Rust.

Rethinking garbage collection

• Claim: "garbage collection is slow" confuses symptom with cause. Garbage collection is just a mechanism for freeing memory no longer needed; fast programs already avoid per-object =malloc=/=free= (slab and arena allocators) and so are halfway to a collector.
• On the JVM all memory is reachable from any thread, so freeing without stopping the world is hard; concurrent collectors (Shenandoah, Azul) are impressive engineering.
• Pony: each actor effectively has its own heap and frees its own memory after doing some work, using a heuristic. No global pause, so latency is flat instead of spiky; the cost is slightly lower peak throughput.
• Difference from hand-written allocators: the programmer is removed from deciding when memory is freed.

What software correctness means

• Definition: the program does what is expected of it, framed as invariants (guarantees); it does its business purpose and "is not going to wake anybody up at 2 in the morning".
• Many teams do not know what they expect the software to do, so they cannot tell when it is working.
• Antithesis is positioned as a software verification and correctness company, not a testing company.

Tests as a means to an end

• Quote from his blog: "No one cares about testing ... Tests are a means to an end. The means are unimportant."
• Manual testing is the worst case; automation gets progressively more sophisticated, but all of it happens late. Better: do as much as possible before testing, via languages and type systems that make incorrect states unrepresentable.
• Ada refused programs that were fundamentally memory unsafe, which is correctness from the start; C gave "a big giant gun pointed at my own foot".

TDD, katas and property-based testing

• Likes TDD as a way to design good APIs.
• In pair-programming katas he played the implementer literally: hardcode the minimal answer per example test (2+2 returns 4, then special-case 2+3). The only way to defeat that is randomized inputs, which leads to property-based testing.
• Colleagues were frustrated but came out writing better tests. Many tested things would not need tests with a stronger compiler.
• Personal arc: loved dynamic languages (Smalltalk, Ruby, Perl, Python) while working on small systems held in one head; value of compiler help became clear on larger systems with more people, e.g. deleting a class in Java and having the compiler list everything that breaks.

Workloads

• Workload: the thing used to validate the system plus the inputs generated to drive it. Naive property-based testing (pick get/put/delete at random) produces a "drunken walk" that never gets far, so it never reaches disk swapping, garbage collection or resharding. A workload has to be designed: key range, key size, value size, distributions that push the system into interesting regions.
• Bank test (classic for ACID isolation): N accounts with a fixed total (10 accounts of 1000), concurrent transfers inside transactions, and a concurrent reader summing all balances; the only legal value is 10000. Passes on a laptop, but with network faults and node kills (Jepsen, Antithesis) many databases show bugs.
• A workload describes rules and lets the exploration work itself out, instead of constructing specific scenarios as in example-based unit tests. It can be discussed abstractly ("the bank test") or as a concrete implementation against a particular database.
• Kyle Kingsbury (Jepsen) made this style famous; Lorin Hochstein's incident write-ups are given as examples of the same failure patterns in production.

Quality is not a gate

• From his post: the gate idea rests on the belief that quality is held by keeping bad out and catching the bug at the door.
• Preferred ordering: model checking and specifications (TLA+, Alloy) in an ideal world; then static guarantees (Pony, Rust, OCaml type systems; Erlang gets there through copying messages between actors instead of types); testing and verification only for what static means cannot enforce. Every language has trade-offs (performance, etc.), so the perfect type system probably does not exist.
• Everyone ends up testing in production; no generator covers corrupted data that exists only in production. A gate where "it passed, so it is quality" is "kind of a lie"; only increasing levels of assurance exist, with holes at every layer.
• Observation: low-functioning teams (slow, or fast with frequent emergency releases) think in pull-request and staging gates; teams that move fast and confidently think about quality from the very start: TLA+ for a consensus algorithm, or a Jepsen/Antithesis-style tool on the very first version before shipping. Fixing early is cheap.
• Gergely's push-back: business-logic correctness and Google Search ranking are hard to specify. Sean's answer: decompose into questions. "Is it working" (a query returns results, correct under 1000 requests per second, concurrent requests, results belong to the right query via markers, no leaking of another user's data) differs from "is the ranking relevant", which is a different problem.

Supply chain security

• Definition: the easiest way to compromise popular software is to attack its weakest link; applies to hardware too (malicious firmware under trusted computing modules).
• Examples: left-pad style package replacements, malware in npm and Python packages, code running in CI/CD with access to all secrets and publishing credentials.
• Naive defenses: cool-down period before consuming new versions (fails if everyone does it, and delays real security fixes), removing dependencies, forking and vetting in-house. None solves the underlying problem.
• Root cause: package management traces back to the trusting design of CPAN and early internet; in nearly every language, imported code has the same capabilities as the author's code and can do anything. Sandboxes can be escaped.
• Direction: object capabilities (Mark Miller's language E; Pony has them built in; recent research from Imperial presented at Bug Bash in Copenhagen): an action such as opening a network connection requires having been handed the capability. The foreign function interface also has to be controlled or it becomes an escape door. No popular language does this, and incremental changes to current ecosystems will not get there.

Side-channel attacks and confidential computing

• Speculative execution gave most CPU speed-ups of the last 20+ years, but speculative branches exist in memory and can be read through side channels, including keys.
• Confidential computing: run software where the operators of the environment are not trusted (cloud employees can be phished, bribed or be agents of governments; the Twitter-Saudi case is cited). Fewer trusted parties means a more secure system.
• Sean worked in the confidential computing group at Microsoft Research (confidential container offering); every guarantee came with "modulo side-channel attacks". Fully closing the hole would mean removing speculative execution; after early kernel patches (the first cost roughly 50 percent performance) the industry settled into whack-a-mole. Sean admits to exploiting branch prediction in his own open-source code: the speed-up is too attractive.

Technical debt revisited

• Quote from his post a decade earlier: the debt metaphor is misleading; debt only hurts if it has to be paid back. Still stands by it.
• Example: heavy debt around MySQL sharding limits was sidestepped by paying for a distributed database that looks like a single database, with rare edge cases in guarantees that did not matter for that company. Other outcomes: the system is no longer needed after 3 years, or the company does not find product-market fit, so the debt never matters.
• Gergely's Uber example: an Uber Eats engineer deleted a failing test in shared code, which looked reckless until the division was sold 6 months later; the engineer optimized for tomorrow.
• Distinction: hacking something in versus building something quickly that covers a tiny sliver, is easy to remove, and does not slow five later additions. Sometimes the cost is paid, usually because the product succeeded. The claim that every bit of debt must be repaid "is not borne out in reality".
• Goal is malleable software: able to adapt to a changed environment, where one valid answer is throwing the thing away.

Going slow to go fast

• Items from his post: write a planning document and agree before touching code; know how the thing will be tested before building; spend hours or days on throwaway spikes for unknown parts; stop when production is on fire at 2 a.m.
• Working 80 hours a week yields mistakes and bug hunting instead of progress; stepping away when tired is part of going fast.
• Biggest time waster: people using the same words with different meanings. Example: the distributed-systems argument about "exactly once", where one side meant exactly-once processing (idempotence) and the other exactly-once arrival of messages. Another: a ticket card handed over, 5 days of work, "that is not what we expected".
• Agile sprints were meant to bake in regular agreement checks. For a large thing, the first days should be writing down how it works and what it does, when changes are cheap.
• Design for knowing it works from the beginning: observability, detection of outages and gray failures (service up and pinging the load balancer while many users have a bad experience), static guarantees. Small up-front investment, alignment, then fast execution.