Ryan Brewer's Blog - Ryan Brewer

Blog Posts

  • The Cricket Language

    September 12, 2024

    Cricket is a lazy gradually-typed functional language with objects. It's very tiny but very expressive; anyone can implement it themselves!

  • Getting Started with Category Theory

    July 29, 2024

    Category theory is a beautiful and powerful field but it can feel impenetrable without the right entry point. This post hopes to serve as a sort of beginner's guide and reference.

  • The Type of Sprintf

    May 14, 2024

    Most static type systems wouldn't let you make something like sprintf, whose type is determined by a format string. Dependent types can save the day!

  • Simple Programming Languages

    March 20, 2024

    Simple programming languages are wonderful to work in. But what is it about them that actually makes them simple? And why do we like that so much?

  • Advanced Typechecking for Stack-Based Languages

    February 18, 2024

    This post discusses the interesting typechecker of SaberVM, which uses a stack-based bytecode language with a powerful type system.

  • A Beginner's Guide to Programming Language Academia

    January 28, 2024

    This post briefly maps out many different subfields of programming language theory, in an effort to make it more accessible to those outside academia.

  • Safe Manual Memory Management with Coeffects

    January 25, 2024

    Using ideas from Crary et al.'s Calculus of Capabilities, I discuss the coeffectful memory management used in SaberVM.

  • Announcing the Saber Virtual Machine

    January 18, 2024

    This post announces SaberVM, an abstract machine for functional programs that guarantees safety, reliability, and portability.

  • Security and Crashing with Modal Logic

    December 17, 2023

    Modal logic is a beautiful field of logic that can be applied to computer science in a few ways, one of which we explore in this post. It can elucidate security concepts and how and why to crash software.

  • Implicit Products: A Better Type-Theoretic "Forall"

    December 10, 2023

    Implicit products are a fascinating approach to universal quantification in dependent type theory, as well as proof irrelevance/erasure in compiler implementation.

  • An Introduction to Proofs with Dependent Types

    December 3, 2023

    This post introduces the basic ideas behind dependent-type-based proof assistants, and expressing logic with types and values.

  • My First Blog Post

    November 16, 2023

    A test post for the blog.