A place for musings, observations, design notes, code snippets - my thought gists.
Euclidea: An interactive geometric theorem prover
After watching the excellent piece of exposition on mathematical exploration by 3Blue1Brown guest Ben Syversen: “What was Euclid really doing?”, I discovered the fantastic web and mobile game Euclidea.
Geometry was never my favourite branch of mathematics, I always felt more drawn to algebra and more symbolic and abstract forms of reasoning. But Euclidea really does a masterful job of capturing the joy of exploration and problem solving through the lens of scaffolded puzzles of compass-and-straightedge geometric constructions.
As you construct each solution, they get encapsulated and added to your toolkit of re-usable constructions. It’s a best way to demonstrate the power of axiomatisation and iteratively increasing the levels of abstraction.
Recursive problem solving with DNS
I really enjoyed this Learning DNS in 10 years talk by Julia Evans. Not only does it present a great, lightweight walkthrough on DNS, but it espouses a maxim for learning I really appreciate: keep digging, and when you get stuck, keep digging.
Rust for everyone [video]
A while ago I mentioned that I thought that Rust was a fiendishly complex language at first glance. Well, that hasn’t changed. Don’t get me wrong, I love Rust, and I wish I had the time to dive deeper into it, but it has a steep learning curve.
That said, I recently came across a fantastic video, “Rust for Everyone”, presented by Will Crichton at Jane Street that explores the various tools he’s built to make Rust more accessible to newcomers. It’s not in the video description, but here’s an outline of the tools Will discusses:
- Aquascope: A tool that provides a visual representation of Rust’s ownership model, making it easier to understand how ownership and borrowing work in Rust.
- Argus: An improved Trait debugger that lets you drill down as much (or as little) as you want through a Trait type-check compiler error.
- Flowistry: I think this is the coolest tool here. It allows you to trace the ’effect-flow’ of your program, highlighting only the sections of code that could possibly affect a selected variable.
The font of all knowledge
TIL that Google Search has a font-based Easter Egg. If you search for “Georgia font”, the results page will change the typeface to Georgia. I initially thought it was limited to System-fonts, but Wikipedia shows that it works for Roboto too!
I discovered this when looking up various fonts for this blog. I initially specified the default browser sans-serif font in my CSS, but ended up switching to Georgia for the text-body as I find it more readable for longer posts. There are some beautiful fonts in Google Font I’d love to use, but for now I’m going to stick with the System Font Stack to avoid loading more external resources on page-load.
From Lambda Calculus to Lifelong Learning
About a decade ago, whilst meandering through a late-night Wikipedia rabbit holeSome things haven’t changed at all, I stumbled across the page for the Lambda Calculus.
A small footnote linked to An Introduction to Lambda Calculus and Scheme, a transcript of a short talk presented by Jim Larson, and, well, I fell in love. I loved the fact that there was this beautiful correspondence between foundational mathematics and models of computation; and that you could describe it through these symbolic wrappers called Lambda terms. There was something deep and abstract about it that I felt immensely drawn to.
The fact that you could start with primitive definitions like
$$ \begin{cases} \textsf{true} &= \lambda x.\lambda y.x \\ \textsf{false} &= \lambda x.\lambda y.y \end{cases} $$and with a couple of basic reduction operations (\(\alpha\)-reduction and \(\beta\)-reduction) construct the ternary conditional:
$$ \textsf{if-then-else} = \lambda a.\lambda b.\lambda c.((a)b)c $$just blew my mind. I’m not completely sure, but I think looking up the Y-combinator is how I ended up discovering Hacker News and began my lifelong, monotonically increasing tab-count trajectory.
Fast forward to university, and I had the pleasure of studying the Lambda Calculus in a more crystallised form, where I fell in love a second time - this time with Haskell.
And now? Well, now you’re reading this post on a blog called Abstract Nonsense, a subject of layers of abstraction, much like the calculus that inspired it.
Speaking of abstraction, if you haven’t had a chance to read the excellent post Up and Down the Ladder of Abstraction by Bret Victor, go and read it now. It’s superb.He’s even got a post on the Lambda Calculus!
The endless procrastination of meta-blogging
I came across this great piece on the act of blogging. Since I started pursuing blogging as a practice, it’s been a very rewarding experience. But my drafts and ideas list is ever growing and my output of substantive content is decreasing proportionately.
I’ve learnt a lot from the simple act of setting up my blog in the first instance: from quality learnings about internet networking through to the dreaded menagerie of tooling that frontend developers call ’the web’. But I can’t deny I spend far too much time blogging about blogging than I do actually blogging (this post is no exception).
This succinct graphic visualises the blog-metablog tragedy:
I mean to change this, I really do. I just can’t deny it’s far easier to sit down and feel productive by fixing yet-another website presentation bug than it is to actually be productive by sitting down to write quality content. This is the tyranny of meta-blogging. But good content doesn’t come without discipline and effort, and I am vowing to myself to reverse the balance.