Blog | Brandon Rozek

From Alex’s blog post, I’ve learned that there are enough recent breakthroughs in quantum computing that I should take post-quantum cryptography seriously.

I recently updated all my geo-distributed web servers to run on Fedora CoreOS (yes, I still love it).

A few month’s ago, Brad Reese, the grandson of the founder of the Reese’s company, called the company out for swapping out the chocolate and peanut butter in some of their products.

Meet Giraffe.

As an example, he asked me, in more words, what the expected rank when flipping over the top card of a deck of cards was (A=1, J=11, Q=12, K=13).

I believe in the freedom of information.

In 2020, Clare and I got our first live Christmas tree.

We have many ways to share ideas today.

For the past year, I settled on a backup strategy that serves my needs.

Back in August, I started running regularly and recording my sessions.

Let’s play Mario Party tonight!

I have a VPS whose contract ends in December.

Nested cases in proofs increase cognitive load for the reader since they have to process not only the case recently stated but also all the case splits prior.

My friend Ethan recently wrote a blog post on cursed commands.

Say we have a set that we want to iterate over within a pure Dafny function.

Nowadays it seems like every tech company is eager to scrape the web.

Last weekend, on my way back north from visiting downtown, I took a break near the Crestview lightrail station.

It’s summer and I’m currently in Austin, Texas, where the temperature ranges between 85 F when we had a recent thunderstorm to 100 F when there are no clouds in the sky.

The Curry-Howard Correspondance establishes a direct connection between computer programs and mathematical proofs.

This blog post is inspired from a lecture that Dr.

The first level within the five levels of configuration languages is a string in a file.

When verifying proofs about code, I often end up with a hypothesis that has an if statement in it.

On April 16 2015, I wrote my first two blog posts on creating responsive layouts in CSS.

I woke up this morning to a small layer of snow outside.

Open WebUI provides a nice chat interface for interacting with LLMs over Ollama and OpenAI compatible APIs.

The United States National Weather Service (NWS) has a JSON API which provides weather alerts and forecasts for free without having to create an API key1.

For two years now, my friend and colleague James Oswald has told me to check out WebAssembly.

Catching up on my RSS feeds, Ava’s bear blog question challenge has been making the rounds.

When I go to download Fedora Workstation 41, it gives me an option to verify the ISO download with a SHA-256 checksum. a2dd3caf3224b8f3a640d9e31b1016d2a4e98a6d7cb435a1e2030235976d6da2 The idea is that when I download the ISO, I run sha256sun Fedora-Works…

The transitive closure of a binary relation cannot, in general, be expressed in first-order logic (FO) In Ray Reiter’s book “Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems”, he goes over a typical naive encoding…

I noticed when looking at my monitoring that accessing my website from Asia takes almost a full second to load.

Browsing around on the Interwebs, I found that Rahul has a curl card. curl https://codingotaku.com/cc ╔═══════════════════════════════════════════════════════════╗ ║ ) ║ ║ ( (

I don’t know about you, but I don’t particularly enjoy logging onto my router.

Using web service workers, you can set it up so that visitors have an offline experience with your website.

How do you write good?

You know one of the worst errors to deal with on Linux?

Possibility theory is a subset of Dempster-Shafer theory (DST).

Imagine sitting by a tree full of birds.

The following are the steps that I take to replace a hard drive in Btrfs with a drive of equal capacity or larger.

After having a hard drive fail on me once, I’ve been slowly upgrading my homelab to be more resilient.

The jq command is great for quickly viewing and manipulating JSON data.

Prost is a popular Protocol Buffers implementation written in Rust.

One of the fun yearly traditions that Clare and I have is to go apple picking.

Every morning like every good system administrator, I log onto all my machines and type the following command systemctl --failed This gives me a list of all my systemd services that have failed.

When writing Lean code, it’s easier to iterate with unit tests than to prove properties about the function off the bat.

I was reading through the Polymorphism section in the Functional programming in Lean textbook and came across the following example: inductive Sign where | pos | neg def posOrNegThree (s : Sign) : match s with | Sign.pos => Nat | Sign.neg => Int :=…

For my new role, I’ve been learning Rust.

One common approach to securely accessing remote services is to use a VPN.

Gabriel recently released a blog post thinking about the space between a static website and a full-blown CMS.

People want to know where they are within your presentation.