Me.
I'm Ryan Brewer. I'm a passionate software developer working on open-source software for safe, reliable, and portable applications. I specialize in a formal methods approach to systems design, with a focus on ergonomics. In general, my projects aim to be formally memory-safe, fault-tolerant, and very lightweight. Via minimality, I hope to make formal theory more accessible outside the ivory tower of academia, and easier to put into practice where it matters. One of my bigger projects is Arctic, A friendly web framework for easily building fast web applications in Gleam! Arctic powers this website, as well as the one I just linked. If my projects seem cool or valuable in any way, consider supporting my work!
Sponsor
SupportMy Website
This is my website. I use this as a space to store my ideas, advertise myself and my work, and write blog posts about topics that I love. Generally I constrain my posts to be about programming language theory or implementations. Links to my latest posts can be found below. I also have a useful wiki of concepts I've studied, expressed accessibly. A good explanation is the best proof of my own understanding, and an exciting challenge. This website is hosted by Firebase and written in Gleam, and the code is up on my github. Instead of a typical web framework, I wrote my own web framework called Arctic on top of the amazing Lustre. Scripting, markup, styles, etc. for this site are all done by me :)
Blog Posts
Par Part 2: Linear Logic
February 11, 2025Linear logic is a beautiful logical system taking advantage of the mechanisms of the sequent calculus. In this post we explore the various meanings of linear logic, and dig deep into the reasoning behind its peculiar development.
Par Part 1: Sequent Calculus
January 13, 2025Sequent Calculus is a way of doing logic that's very explicit and mechanical. It's used as an important system and notation for type theory and logic related to programming languages.
The Cricket Language
September 12, 2024Cricket 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, 2024Category 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, 2024Most 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, 2024Simple 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, 2024This 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, 2024This 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, 2024Using 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, 2024This post announces SaberVM, an abstract machine for functional programs that guarantees safety, reliability, and portability.
Security and Crashing with Modal Logic
December 17, 2023Modal 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, 2023Implicit 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, 2023This post introduces the basic ideas behind dependent-type-based proof assistants, and expressing logic with types and values.
My First Blog Post
November 16, 2023A test post for the blog.
© 2024 Ryan Brewer.