The new year marks a new style of blog posts. Super serious principle engineers can’t be bothered with words and therefore neither can I. Functional Programming Basics After Dependent Type Theory?...

In 2024 I wrote my first post on this blog, on variance. Rereading it I think there is much that can be improved and the whole thing can be shortened, so here it is. Requirements Variance needs t...

All the code snippets in this article are compiled into a fully working proof accessible here You can read Part II here Our previous ventures into type theory were all self-motivated and hig...

Here is my top playlist from 2024. It is titled “Ice cream and hugs” because of a memorable evening when I assembled it from that week’s discover weekly. My favourite songs are all associated wi...

So there’s layers to outsourcing code right. Programmers have been stealing code since there was code to steal. Why reinvent the wheel when a more general version of the problem probably has a bet...

I’ve been putting off writing this particular article for too long. The idea of writing about the cadetship is what inspired me to create this entire blog in the first place. And right now I’m not ...

All the code snippets in this article are compiled into a fully working proof accessible here You can read Part I here Foreword I believe proving that natural addition commutes is a good ex...

This article is the first installment in a series on type theory. Type theory is a field of math that is not typically covered in an undergrad math or CS degree, but is surprisingly beginner friend...

Do you know what an opinionated technology is? The topic came up naturally in conversation at work. It started with some first year cadets talking about projects they were working on before startin...

I am not a mathematician by trade but I have always enjoyed maths as a hobby, and for the longest time have wanted to invent my own math. The way inventing new math typically goes is someone works ...