Write a mathematical proof generator for AoC 1-1 2022

For last year’s AoC, I decided to use 20 different programming languages. For the year before that, I used Haskell. This year I decided to not participate as I’m already busy with other stuff, but I thought I could try something different.

So the first task of AoC day 1 is essentially giving you a list of lists, and you need to sum each element and find the max. Here’s a one-liner in Python:

max([ sum(x) for x in L ])

But I thought to myself, why write code in a “normal” programming language to solve an easy problem? Why not complicate things a little bit and write a code that generates mathematical proof in Budge-TP? In this post, we will write a Python script that will solve AoC 1-1 by generating Budge-TP code.

Continue reading →

GEB: An EGB overview (Part II)

This post is a follow-up to the first part.

However, before proceeding with the usual format as in the previous post, I will make a small comment.

I was very amazed by the first part of the book, so before starting the second part I viewed the book’s references. One book caught my attention: “What is the Name of this Book?”. So I ordered it and I read it. I found the book’s author’s style to be very similar to GEB’s style: puns, self-references, discussions about meaning, and paradoxes. So if you follow GEB’s references, you can almost see how GEB’s author’s style came to be.

Continue reading →

Writing your second program with Budge-TP (complexity and abstraction)

In a previous blog post, we showed and implemented a formal system that was able to represent numbers and the addition operator.

In this blog post, we will show an implementation of a subset formal system of Peano’s axioms that will also be able to represent numbers and the addition operator.

Finally, we will compare both systems.

Continue reading →

Writing your first program with Budge-TP

Budge-TP (bʌdʒ, b’dzh) is a theorem prover (really, just another programming language) that allows you to express formal systems (really, just programs).

In this post, I will show you how to write a simple program in Budge-TP.

Continue reading →

Teaching my kids programming & math

For these exercises, all you need is some creativity and pen & paper.

The crucial bit is to come up with some exercises in order to get their attention. Find what they enjoy playing with, and gamify it. If they like pets, make commands to e.g. feed a pet. If they want toy soldiers games, make commands for e.g. moving and attacking.

Continue reading →