Designing Cyclic Puzzles for Simon Says

I recently participated in the Bevy Jam 5 Game Jam, where the theme was “Cycles”. My take on this idea was Simon Says, a puzzle game where the player character must follow a series of instructions in a loop or cycle to complete the puzzle. While designing puzzles for this game, I quickly discovered a set of interesting mathematical properties underlying the solution space that I’d like to show you....

August 8, 2024 · 6 min · Dylan R. Johnston

Formally Verifying Rust's Opaque Types

Introduction The other day I was reading this blog post covering existential types in Rust (also known as impl Trait or opaque types). In that blog post, the author makes the following claim. We’re going to have to take a slight diversion into type theory here because it motivates a result that is perhaps intuitive. The following proposition holds in intuitionistic logic: ((∃ x. P(x)) → Q) ⇔ (∀ x. (P(x) → Q)), which means that according to the Curry–Howard Correspondence, it also holds when considering the proposition as a type....

August 1, 2022 · 17 min · Dylan R. Johnston

How I Made This Blog

Plan of Attack When evaluating options for starting a blog I wanted something that was fast, free, and easy to setup CI / CD for. GitHub Pages ticks both the free and easy boxes but it can be a bit slow to respond. To solve the speed issue I stuck cloudflare in front of GitHub to leverage its CDN caching, ensuring that response times are fast. ┌ │ │ │ └ ┌ │ └ ─ ─ ─ ─ ─ d ─ ─ U ─ ─ y ─ ─ s ─ ─ l ─ ─ e ─ ─ G a ─ ─ r ─ ─ i n ─ ─ ─ ─ t r ─ ┐ ├ ┘ ─ H j ─ ─ ─ u o ─ ─ ─ b h ─ ─ ─ n ─ ─ ─ R s ─ ─ ─ e t ─ ┌ │ ► │ └ ─ p o ─ ─ ─ ─ o n ─ ─ C N ─ ─ s ....

July 27, 2022 · 4 min · Dylan R. Johnston