A Verified Evaluator for the Untyped Concatenative Calculus
6793 words, about 32 minutes to read.
Earlier, I wrote an article in which I used Coq to encode the formal semantics of Dawn’s Untyped Concatenative Calculus, and to prove a few things about the mini-language. . . .
Formalizing Dawn in Coq
4345 words, about 21 minutes to read.
The Foundations of Dawn article came up on Lobsters recently. In this article, the author of Dawn defines a core calculus for the language, and provides its semantics. . . .
Type-Safe Event Emitter in TypeScript
1067 words, about 6 minutes to read.
I’ve been playing around with TypeScript recently, and enjoying it too. Nearly all of my compile-time type safety desires have been accomodated by the language, and in a rather intuitive and clean way. . . .
Approximating Custom Functions in Hugo
629 words, about 3 minutes to read.
This will be an uncharacteristically short post. Recently, I wrote about my experience with including code from local files. After I wrote that post, I decided to expand upon my setup. . . .
Pleasant Code Includes with Hugo
1822 words, about 9 minutes to read.
Ever since I started the compiler series, I began to include more and more fragments of code into my blog. I didn’t want to be copy-pasting my code between my project and my Markdown files, so I quickly wrote up a Hugo shortcode to pull in other files in the local directory. . . .
Advent of Code in Coq - Day 8
8562 words, about 41 minutes to read.
Huh? We’re on day 8? What happened to days 2 through 7? Well, for the most part, I didn’t think they were that interesting from the Coq point of view. . . .
Advent of Code in Coq - Day 1
3502 words, about 17 minutes to read.
The first puzzle of this year’s Advent of Code was quite simple, which gave me a thought: “Hey, this feels within reach for me to formally verify! . . .
A Typesafe Representation of an Imperative Language
4143 words, about 20 minutes to read.
A recent homework assignment for my university’s programming languages course was to encode the abstract syntax for a small imperative language into Haskell data types. . . .
Compiling a Functional Language Using C++, Part 13 - Cleanup
8232 words, about 39 minutes to read.
In part 12, we added let/in and lambda expressions to our compiler. At the end of that post, I mentioned that before we move on to bigger and better things, I wanted to take a step back and clean up the compiler. . . .
How Many Values Does a Boolean Have?
2079 words, about 10 minutes to read.
A friend of mine recently had an interview for a software engineering position. They later recounted to me the content of the technical questions that they had been asked. . . .
Meaningfully Typechecking a Language in Idris, With Tuples
2220 words, about 11 minutes to read.
Some time ago, I wrote a post titled Meaningfully Typechecking a Language in Idris. I then followed it up with Meaningfully Typechecking a Language in Idris, Revisited. . . .
Time Traveling In Haskell: How It Works And How To Use It
4283 words, about 21 minutes to read.
I recently got to use a very curious Haskell technique in production: [note: As production as research code gets, anyway! . . .
DELL Is A Horrible Company And You Should Avoid Them At All Costs
3694 words, about 18 minutes to read.
I really do not want this to be a consumer electronics blog. Such things aren’t interesting to me, and nor do I have much knowledge about them. . . .
Meaningfully Typechecking a Language in Idris, Revisited
2962 words, about 14 minutes to read.
Some time ago, I wrote a post titled Meaningfully Typechecking a Language in Idris. The gist of the post was as follows: . . .
Rendering Mathematics On The Back End
2242 words, about 11 minutes to read.
Due to something of a streak of bad luck when it came to computers, I spent a significant amount of time using a Linux-based Chromebook, and then a Pinebook Pro. . . .
Compiling a Functional Language Using C++, Part 12 - Let/In and Lambdas
10266 words, about 49 minutes to read.
Now that our language’s type system is more fleshed out and pleasant to use, it’s time to shift our focus to the ergonomics of the language itself. . . .
Building a Crystal Project with Nix, Revisited
1183 words, about 6 minutes to read.
As I’ve described in my previous post, the process for compiling a Crystal project with Nix is a fairly straightforward one. . . .
Compiling a Functional Language Using C++, Part 11 - Polymorphic Data Types
4366 words, about 21 minutes to read.
In part 10, we managed to get our compiler to accept functions that were polymorphically typed. However, a piece of the puzzle is still missing: while our functions can handle values of different types, the same cannot be said for our data types. . . .
Compiling a Functional Language Using C++, Part 10 - Polymorphism
8082 words, about 38 minutes to read.
In part 8, we wrote some pretty interesting programs in our little language. We successfully expressed arithmetic and recursion. But there’s one thing that we cannot express in our language without further changes: an if statement. . . .
Math Rendering is Wrong
1537 words, about 8 minutes to read.
Since I first started working on my website at age fourteen, the site has gone through many revisions, and hopefully changed for the better. . . .
Creating Recursive Functions in a Stack Based Language
1995 words, about 10 minutes to read.
In CS 381, Programming Language Fundamentals, many students chose to implement a stack based language. Such languages are very neat, but two of the requirements for such languages may, at first, seem somewhat hard to satisfy: . . .
Meaningfully Typechecking a Language in Idris
2407 words, about 12 minutes to read.
This term, I’m a TA for Oregon State University’s Programming Languages course. The students in the course are tasked with using Haskell to implement a programming language of their own design. . . .
Building a Basic Crystal Project with Nix
763 words, about 4 minutes to read.
I really like the idea of Nix: you can have reproducible builds, written more or less declaratively. I also really like the programming language Crystal, which is a compiled Ruby derivative. . . .
Compiling a Functional Language Using C++, Part 9 - Garbage Collection
4807 words, about 23 minutes to read.
“When will you learn? When will you learn that your actions have consequences?” So far, we’ve entirely ignored the problem of memory management. . . .
Using GHC IDE for Haskell Error Checking and Autocompletion
627 words, about 3 minutes to read.
Last year, when I took Oregon State University’s CS 381 class, I ended up setting up my editor with the Haskell IDE engine. . . .
A Language for an Assignment - Homework 3
4138 words, about 20 minutes to read.
It rained in Sunriver on New Year’s Eve, and it continued to rain for the next couple of days. So, instead of going skiing as planned, to the dismay of my family and friends, I spent the majority of those days working on the third language for homework 3. . . .
A Language for an Assignment - Homework 2
1927 words, about 10 minutes to read.
After the madness of the language for homework 1, the solution to the second homework offers a moment of respite. Let’s get right into the problems, shall we? . . .
A Language for an Assignment - Homework 1
3900 words, about 19 minutes to read.
On a rainy Oregon day, I was walking between classes with a group of friends. We were discussing the various ways to obfuscate solutions to the weekly homework assignments in our Algorithms course: replace every if with a ternary expression, use single variable names, put everything on one line. . . .
1175 words, about 6 minutes to read.
A friend recently showed me a website, the design of which I really liked: Gwern Branwen’s personal website. In particular, I found that sidenotes were a feature that I didn’t even know I needed. . . .
Compiling a Functional Language Using C++, Part 8 - LLVM
4847 words, about 23 minutes to read.
We don’t want a compiler that can only generate code for a single platform. Our language should work on macOS, Windows, and Linux, on x86_64, ARM, and maybe some other architectures. . . .
Thoughts on Better Explanations
942 words, about 5 minutes to read.
How do you explain how to write a program? Instructional material is becoming more and more popular on the web, with thousands of programming tutorials for languages, frameworks, and technologies created on YouTube, Medium, and peole’s personal sites. . . .
Compiling a Functional Language Using C++, Part 7 - Runtime
2160 words, about 11 minutes to read.
Wikipedia has the following definition for a runtime: A [runtime] primarily implements portions of an execution model. We know what our execution model is! . . .
Compiling a Functional Language Using C++, Part 6 - Compilation
4949 words, about 24 minutes to read.
In the previous post, we defined a machine for graph reduction, called a G-machine. However, this machine is still not particularly connected to our language. . . .
Compiling a Functional Language Using C++, Part 5 - Execution
4438 words, about 21 minutes to read.
We now have trees representing valid programs in our language, and it’s time to think about how to compile them into machine code, to be executed on hardware. . . .
Compiling a Functional Language Using C++, Part 4 - Small Improvements
2117 words, about 10 minutes to read.
We’ve done quite a big push in the previous post. We defined type rules for our language, implemented unification, and then implemented unification to enforce these rules for our program. . . .
Compiling a Functional Language Using C++, Part 3 - Type Checking
5793 words, about 28 minutes to read.
I think tokenizing and parsing are boring. The thing is, looking at syntax is a pretty shallow measure of how interesting a language is. . . .
Switching to a Static Site Generator
574 words, about 3 minutes to read.
A long time ago, I decided to try out Jekyll for my website. However, it all felt too convoluted: the ruby gems I needed to install, the configuration options for the site, the theming. . . .
Compiling a Functional Language Using C++, Part 2 - Parsing
3658 words, about 18 minutes to read.
In the previous post, we covered tokenizing. We learned how to convert an input string into logical segments, and even wrote up a tokenizer to do it according to the rules of our language. . . .
Compiling a Functional Language Using C++, Part 1 - Tokenizing
1788 words, about 9 minutes to read.
It makes sense to build a compiler bit by bit, following the stages we outlined in the first post of the series. . . .
Compiling a Functional Language Using C++, Part 0 - Intro
971 words, about 5 minutes to read.
During my last academic term, I was enrolled in a compilers course. We had a final project - develop a compiler for a basic Python subset, using LLVM. . . .
Local Development Environment for JOS and CS 444
733 words, about 4 minutes to read.
Working with the instructor’s dotfiles on the server is great and all, but there’s a few things you can do loccally that you can’t do on the school server: . . .
Lambda Calculus and Church Encoded Integers
1847 words, about 9 minutes to read.
You always hear the words “turning complete” thrown around in various contexts. Powerpoint is Turing complete, CSS is Turing complete. Turing completeness effectively describes a property of a language of system to perform any computation that can be performed on a computer (or by a human with a piece of paper). . . .
Proof of Inductive Palindrome Definition in Coq
1408 words, about 7 minutes to read.
Going through the Software Foundations textbook, I found an exercise which I really enjoyed solving. This exercise was to define an inductive property that holds iff a list is a palindrome. . . .
Setting Up Crystal on ARM
792 words, about 4 minutes to read.
Having found myself using a Chromebook with Arch Linux, I acutely felt the lack of official Crystal builds for ARM. After spending an hour or so looking online for a comprehensive guide to getting a working compiler on ARM, I think I now know the general idea. . . .
Haskell Error Checking and Autocompletion With LSP
1550 words, about 8 minutes to read.
For Oregon State University’s CS 381, Programming Language Fundamentals, Haskell is the language of choice. While it has an excellent REPL, and an excellent compiler, a piece of the puzzle is missing when writing Haskell code: on-the-fly error checking. . . .
A Look Into Starbound's File Formats
2080 words, about 10 minutes to read.
After playing a few hours of Starbound, I decided that I wanted to mess around with its file format, perhaps make a save manager/swapper, or something. . . .
New Look, New Features!
107 words, about 1 minutes to read.
I’ve recently taken the time to redesign my website from scratch, on both the back-end and the front-end! On the back-end, this means the addition of tags, which allow me to categorize the not-so-plentiful content on the site. . . .
Learning Emulation, Part 2.5 - Implementation
851 words, about 4 minutes to read.
This is the third post in a series I’m writing about Chip-8 emulation. If you want to see the first one, head here. . . .
Learning Emulation, Part 2
649 words, about 4 minutes to read.
This is the second post in a series I’m writing about Chip-8 emulation. If you want to see the first one, head here. . . .
Learning Emulation, Part 1
570 words, about 3 minutes to read.
I’ve decided that the purpose of a blog is to actually use it every once in a while. So, to fill up this blank space, I’ll be documenting my own experience of starting to learn how emulation works. . . .