Readings

This page contains a collections of interesting resources, across a variety of topics. My main criterion for posting here is that I found it interesting or useful. My only rule is that I have to have actually read it to post it here. Suggestions always welcome. Page inspired by the great one at mcyoung.xyz .

Programming Language Theory/Type Theory

Resources on the formal definitions of programming languages and type systems. While real languages are always more than theoretical models, it’s essential to ground in these models. You can prevent making mistakes that have been made before, have consistency in your design, and make sure that your type system actually guarantees something.

• By the god Benjamin Pierce
  • Software Foundations The first two volumes have you learning the Coq proof assistant and build up to your formalizing and proving things about simple imperative and functional languages, as well as a simple type system and all of the basic extensions. It’s a great foundational text. (Many more people than just Benjamin Pierce contributed to this)
  • Types and Programming Languages TAPL is a masterpiece. It goes into greater depth on topics than SF, at the cost of not all being formalized in Coq.
  • Advanced Topics in Types and Programming Languages ATAPL Covers a bunch of the wacky things not covered in TAPL, such as: types systems for assembly languages, dependent types, substructural types.
• Programming Languages: Applications and Interpretations Introduces a wide variety of languages features and ideas via simple interpreters.
• The Little Typer A very cool Socratic style introduction to dependent type theory
• Interpreters Chapter from SICP Fun chapter on implementing a core interpreter for a simple functional language and expanding it with wacky features

Programming Language Design

Moving away from considering languages as abstract mathematical objects, this is a series of posts that talk about language design .

• Let Futures Be Futures Notes on the design of async Rust.
• Ownership How to take advantage of substructural type systems in a language
• References are like jumps on how languages can enable or interfere with “local reasoning” about whether your program is correct
• Oxidizing OCaml Locality and Ownership . Two great posts on retrofitting a more performant semantics into OCaml.
• The Rust I wanted had no future Essay from Graydon Hoare, the original creator of Rust, about how the project has diverged from where he thought it would go. Talks about why it diverged and how.
• I want off Mr. Golang’s Wild Ride on how languages (and specifically their standard libraries and type systems) can help make software either robust or fragile.

Compilers

Notes on (usually optimizing) compilers. Fast languages use compilers. Compilers are cool. I like compilers.

• MinCaml Paper on a nice simple compiler for functional languages.
• CS 6120 Not a reading, but a set of lectures.
• A Guide to Undefined Behaviour in C and C++ , and Part 2 ,and Part 3 A guide to thinking about what undefined behaviour means. An important quote form the article:

It is very common for people to say — or at least think — something like this: The x86 ADD instruction is used to implement C’s signed add operation, and it has two’s complement behavior when the result overflows. I’m developing for an x86 platform, so I should be able to expect two’s complement semantics when 32-bit signed integers overflow. THIS IS WRONG. You are saying something like this: Somebody once told me that in basketball you can’t hold the ball and run. I got a basketball and tried it and it worked just fine. He obviously didn’t understand basketball.

• What Every C Programmer Should Know About Undefined Behaviour and Part 2 Part 3 Explains a lot of the optimizations that undefined behaviour enables. If you’re a language safety advocate (like me), it’s important to understand this.
• Notes on Type Layout and ABIs in Rust and How Swift Achieved Dynamic Linking Where Rust Couldn’t and C isn’t a Programming Language Anymore The best collections of articles on dynamic linking/ABIs.
• Formal verification of a realistic compiler The CompCERT project: a formally verified compiler for C
• Proving the correctness of a compiler By the same author as the above, but about a much simpler language
• The implementation of functional programming languages Implementing a compiler/runtime for a lazy,functional programming language (think Haskell)

Security

• Building a HashMap in Rust I promise this is actually a security article
• What is memory safety Getting a good rigorous definition of memory safety
• Software Security is a Programming Languages Issue Makes the argument that PL theory/design is essential for improving the security of the ecosystem.
• Cedar: a new language for Authorization Paper on the Cedar language I was (and am) involved with designing

Automated Reasoning/Formal Methods

This topic is really cool. It’s also frustratingly opaque. There is no equivalent of “software foundations” for other AR techniques, and that’s a shame.

• CSE 507 - Computer Aided Reasoning for Software Great course
• The Rosette Guide A cool tool for solver assisted programming
• Formal Methods: Just Good Engineering Practice?
• Formal Methods only solve half my problems
• Decision Procedures by Daniel Kroenig
• Handbook of Satisfiability, second edition

Things That Will Bite You

• The Absolute Minimum Every Software Developer Must Know About Unicode ASCII is dead. This isn’t that complicated if your read it.
• Text Rendering Hates You
• Falsehoods programmers believe about timezones

Systems - distributed or otherwise

• Atomic Commitment: The Unscalability Protocol
• Not Just Scale What’s the point of this cloud thing anyway?
• Metastable Failures in Distributed Systems
• IronFleet: Proving Practical Distributed Systems Correct
• What Goes Around Comes Around Short history of data models

Software Engineering

• Parse, don’t validate
• Software Reliability : What Is Property-Based Testing? Introduction to property based testing.
• Choosing Properties for Property Based Testing
• How we build Cedar: A Verification Guided Approach Paper on our development methodology for Cedar