Summer Log
This is a log of my summer (2024) projects. It's my immodest way of enforcing productivity. Feel free to reach out if you want to talk about anything below.
Reading
- How Do We Look, Mary Beard
- Thus Spoke Zarathustra, Friedrich Nietzsche
- The Lily of the Field and the Bird of the Air, Søren Kierkegaard
- Elm Guide, Evan Czaplicki (link)
- Angels and Saints, Eliot Weinberger
- Art in the After-Culture, Ben Davis
- The Threepenny Opera, Bertolt Brecht
- The Pillowman, Martin McDonagh
- Crime and Punishment, Fyodor Dostoevsky
- Adorno, Foucault and the Critique of the West, Deborah Cook
- Means and Ends, Zoe Baker
Projects
- Visualizers for Stack-Oriented Languages
- While teaching CS320, I spent a lot of time walking through the evaluation of stack oriented languages. I'd like to use Elm to build nicer visualizations of this process.
- A rudimentary prototype
- A slightly more interesting prototype
- A mock-up playground for a simple language
- Overture: A Personal Agda Library
- I'd like to spend more time digging into the Agda standard library. As an exercise in library management, I'm also extending it.
- Disclaimer. I have no intention of maintaining this beyond personal use.
- The repository
- Fermat's Little Theorem in Agda
- For their final project, a student in CS400 attempted to prove Fermat's little theorem in Agda (without the standard library). I was impressed by how far they got, but eventually things get tricky when you start reasoning about summations. I decided to put together a proof myself using the standard library. It was hairer than I expected…
- The proof appears in the Overture repository.
- Diane: A Toy Stack-Oriented Language
- I built my first larger-scale prototype of a visualizer for a stack-oriented language
- The website