Blog | Brandon Rozek

Brandon Rozek · brandonrozek.com · English

Software Developer, Researcher, and Linux Enthusiast.

json

Open the feed

https://brandonrozek.com/blog/index.json

Last post: Jun 15, 2026
Posts in 24 h · 7 days · 30 days: 0 · 0 · 0
Our last check: Answering
Served from: Canada
Site title: Brandon Rozek
Text score at discovery: 8,646
Format: json

Posts

What our queue read from this feed. Open one to read it here, or go to the site that published it.

On Post-Quantum Security Adoption
Jun 15, 2026 · original
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. Google and Cloudflare both set a target of 2029 for having their systems secure against quantum computers. Similarly, the UK government is targeting 2035. The issue is that cryptography is built upon math problems that are difficult to solve. Quantum computers make solving some of these problems such as integer factorization and discrete logs easier. If someone has a quantum computer that can sufficiently solve those two problems, then they can likely decrypt many ciphertexts that were produced using asymmetric cryptography techniques (think public/private key-pairs). Wikipedia has a great article discussing post-quantum cryptography if you want to read more. Given all that, if the cost isn t too high then it s not a bad idea to look
Synchronizing my Static Website with Object Storage
Jun 13, 2026 · original
I recently updated all my geo-distributed web servers to run on Fedora CoreOS ( yes, I still love it ). This gave me an opportunity to revisit how I handle synchronization. Before, I used Syncthing which while awesome is a pain to configure. I don t update my website or certs too frequently so having an always online setup seemed overkill. So this time I went with an object storage setup. I created a bucket (e.g my-website ) and within it I have the following directories my-website ├── etc └── letsencrypt └── live └── example.com ├── cert.pem ├── chain.pem ├── fullchain.pem └── privkey.pem └── var └── www ├── website1 ├── website2 └── websiten The core idea is that the webservers will read from this object store to stay up to date with my SSL certificates and my static website files. The rest of the post will go over how I 1) modified my deployment pipeline to push to the object store, 2
Can you tell the difference? A quick look into discrimination testing.
May 24, 2026 · original
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 . The newer ingredients chocolate candy and peanut butter creme are only imitations. But today, REESE S identity is being rewritten, not by storytellers, but by formulation decisions that replace Milk Chocolate with compound coatings and Peanut Butter with peanut‑butter‑style crèmes across multiple REESE’S products. - Brad Reese Jonathan Deutsch over at the Conversation wrote that product reformulations in foods are common and most of the time we don t even notice . This along with shrinking the size of the product are the two main approaches companies use to reduce costs. Discrimination Testing for Food So how can companies be confident that few will notice? That s where discrimination testing comes in. From
Praise the Smart Button
May 22, 2026 · original
Meet Giraffe. Equipped with an Innr AE 270 T smart bulb, it allows me to turn the light on and off from our phones using Home Assistant . The main issue? I need my phone to turn it on and off. Now don t get me wrong, I can still walk up to the lamp and flip the switch. But, then I need to walk back up to it in order to turn it back on. Turns out, the smart bulb needs some power to receive control messages via the network. If that wasn t annoying enough, flipping the switch off would mess with my cool automations. At sunrise, it s supposed to turn on to help wake me up and then automatically turn itself off after noon. So I lived with that reality for a few years. Whenever I want to turn on or off the lamp, I would pull out my phone. Forgot to turn off the lights when I left the house? No worries, I can still control it remotely. But that all changed this Christmas when my wife gifted me
Expectations are Linear
Apr 26, 2026 · original
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). This is easy to compute directly as 7. Then he asked me the expectation of the sum of the top two cards . - From Expectation and Copysets by Justin Jaffray What does your intuition say the answer is? Justin continues by stating that computing this expectation is as easy as summing their individual expectations. $$ E[X + Y] = E[X] + E[Y] $$ In other words, expectations are linear . I recommend reading his entire blog post. It s great and also talks about how this property is used in databases today. After a high-level explanation, he says: The fact that expectation is linear is easy to show if you just look at the definition, which we will not do here, but I trust you are capable of if you are interested and have not already seen it. In this epi
Bringing this website to the Tor network
Feb 1, 2026 · original
I believe in the freedom of information. By making my website available as a Tor hidden service, you can be sure to access the information even if it s blocked on the clearweb. In this post, I ll share the steps I took and what I learned along the way. Huge credit to Christian who wrote their own succinct version of this post and helped me troubleshoot via email. Getting an Address Unlike the clear web, we don t register a domain with anyone. An address on Tor is a hash of your public key. This is why onion URLs are long and unreadable. Take a look at the following onion URL which takes you to the Tor homepage. http://2gzyxa5ihm7nsggfxnu52rck2vv4rvmdlkiu3zzui5du4xyclen53wid.onion Notice that the address starts with http . Unlike the clearweb, all traffic via Tor is encrypted. Our hidden service will use the public key behind the URL during the protocol exchange. The primary benefit of th
Tales of Christmas Trees
Jan 25, 2026 · original
In 2020, Clare and I got our first live Christmas tree. We were living in Virginia at the time, and we showed up to a farm that had many trees planted in rows. They gave us a bow saw, and it was up to us to chop one down and bring it home. I enjoyed having a live tree in my apartment. I still remember the smell of fresh conifer. After several weeks, the holidays pass and the needles start falling to the ground. I don t quite remember how we got rid of this tree, but I wouldn t be surprised if we just threw it in our dumpster. We later moved to New York. For the next few years, we would travel to see friends and family during the holidays. I used that as an excuse to not have a tree setup at home. Eventually Clare convinces me that we should still be festive at home, and we bought a plastic tree. Around us in upstate New York, there are several bonfire events in January. There s one in pa
Blogging as an Invitation for Dialogue
Jan 15, 2026 · original
We have many ways to share ideas today. We can: Text Email Pen a letter Post on a microblog (Mastodon/X/Pixelfed/etc.) Write a blog post But not all of these methods inherently create a conversation or dialogue. When I write a technical blog post, I don t expect a reply. Similarly, when I toot on Mastodon, I m fine if no one favorited the post. As such, (micro-)blogging differs greatly from texting and calling someone and is instead much closer to recording a postcast or uploading a video – a one-way transmission of information. Ploum wrote about how he views the ActivityPub protocol as a conversation , and as such servers should not filter posts based on whether they have a picture . Now I m not on Pixelfed, so I do not have a stake in this issue. However since I view Pixelfed as a microblogging platform, I tend to see it as more of a one-way transmission of information rather than soli
Backing up my data with Restic, Btrfs, and MinIO
Dec 30, 2025 · original
For the past year, I settled on a backup strategy that serves my needs. In this post, I ll share the properties I look for in a backup solution and how my current solution addresses them. As always, if you have any suggestions or improvements, feel free to get in touch. The first step before talking technology is to identify exactly what data we want to backup. In my homelab, I rely on Immich for photo storage, Navidrome for music streaming, databases for my website, and other personal documents. This amounts to a little over 250 GB of data that would be very difficult for me to replace if it was lost. Not all my data lives on that one server though. I also have a storage VPS which runs Nextcloud and Hedgedoc . Both of those services combined have less than 100 GB of data, but just like the homelab, that data is precious. The storage VPS has a total capacity of 1.5 TB. The 3-2-1 backup s
After 75 Miles of Running
Dec 26, 2025 · original
Back in August, I started running regularly and recording my sessions. I recently completed a total of 75 miles of running across all my sessions. In this post, I ll reflect on my journey so far and what I ve learned. The Beginning Over the summer, I lived and worked in Austin, Texas. For the prior months of the year, I ve lived a fairly sedimentary lifestyle. I enjoy these summers where I am forced to walk more places and take public transit since I don t have access to a vehicle. Two of my coworkers were really into running and one of them even regularly ran a few miles outside in the 95+ degree Fahrenheit weather . This didn t immediately convince me to start myself, but it definitely planted the seed. Towards the end of the summer, I asked myself What s stopping me from running? and took this as an opportunity to prove something to myself. What do I need to get started? At the beginn
Disabling Nat Source Port Randomization on OPNsense for Gaming
Dec 23, 2025 · original
Let s play Mario Party tonight! After many years of friendship, I ve learned that playing online multiplayer games is almost never as simple as it seems. This night was no different. In this post, I ll go over what I learned setting up my Nintendo Switch for online play. Luckily, this same concept applies to the PlayStation 5 as well 1 . But first, I ll take a detour into how peer-to-peer (P2P) gaming typically works. So, feel free to skip down to the solution. Peer-to-Peer Gaming Mario Party is a board game where you move characters around in hopes of collecting the most stars. You play as a character from the Mario franchise, and between each turn on the board is a minigame. These minigames provide the illusion that this is a skill-based game. But trust me, you can win by just tapping A. Sony and Nintendo both aren t forthcoming with information about how their games and systems work.
Fedora CoreOS: First Impressions
Nov 28, 2025 · original
I have a VPS whose contract ends in December. Instead of renewing, I decided to switch providers of that VPS to OVHCloud. The latter s commitment to sustainability through renewables and component reuse is super cool. Now, I could ve kept the migration simple and keep the configuration the same. I don t write about it much here, but I have Ansible playbooks for all my servers. However, immutable Linux distributions have been receiving a lot of attention over the past few years and tragically I knew little about them. What is an immutable Linux distribution? It is a Linux distribution with a read-only core. This prevents accidental modifications which overtime lead to an unstable system. There are many different options for these immutable distributions, but as you can see from the title of this post, I went with Fedora CoreOS . The reason is simple. All my other servers run Fedora Server
Flattening Cases to Avoid Nesting in Lean 4
Oct 5, 2025 · original
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. That s why if I can, I prefer to flatten out my cases so that we can see in one step all the variables we re segmenting. I came across this recently in Lean when working on Lattice proofs over integers with $\infty$ and $-\infty$ In Lean, we can define this extended integer ( EInt ) by using WithTop and WithBot import Mathlib.Order.Interval.Basic -- An Integer with a top (∞) and bottom (-∞) element def EInt : Type := WithBot (WithTop Int) deriving LinearOrder @[simp] def EInt.ninf : EInt := (⊥ : WithBot (WithTop Int)) @[simp] def EInt.inf : EInt := (WithBot.some ⊤ : WithBot (WithTop Int)) notation "-∞" = EInt.ninf notation "∞" = EInt.inf -- Helper instances so I can later write numbers and have them casted instance: IntCast EInt wh
Cursed Knowledge: Javascript Arrays Are Objects
Sep 1, 2025 · original
My friend Ethan recently wrote a blog post on cursed commands . Chris shared with me that Immich has a page on their site called cursed knowledge , and it looks like this has started a trend. I ve seen my fair share of the dark arts in programming, so I ll hop on and share what I know about JavaScript arrays. JavaScript arrays are exotic objects according to the ECMAScript specification. Therefore, they may lead to unintuitive behavior if we think of these arrays as C-like. Let s play around. Concept 1: JavaScript arrays are not continguous First, consider the following array: let x = [ 0 , 1 , 2 ]; As one might expect, x.length is equal to 3 . To tell whether or not an index is in an array, we can use the in operator. 3 in x // Evaluates to false If we try to access the 3rd index, the result will evaluate to undefined . x [ 3 ] // Evaluates to undefined Now let s assign an element to th
Deterministically Iterating over a set within Dafny functions
Jul 6, 2025 · original
Say we have a set that we want to iterate over within a pure Dafny function. For sake of example, we will look at a set of strings. In Dafny, var x :| condition denotes let us define variable x such that [condition] . Therefore, a first attempt at writing our function might be: function iterate_helper(collection: setstring, acc: seqstring): seqstring { if collection == {} then acc else var x :| x in collection; var newAcc := acc + [x]; var newCollection := collection - {x}; iterate_helper(newCollection, newAcc) } The issue is that Dafny will complain with the following error message: to be compilable, the value of a let-such-that expression must be uniquely determined Dafny functions must be deterministic. This means that no matter how many times we call a function with some specified input, we will always get the same output. Therefore, as the error message suggests, we need to write a
Dealing with Web Scrapers
Jul 2, 2025 · original
Nowadays it seems like every tech company is eager to scrape the web. Unfortunately, it seems like 1 the majority of traffic that comes to this small site are scrapers. While my static website is able to handle the load, the same cannot be said about everyone. Overall, the techinques I ve seen website owners use aim to make scraping more difficult. Though it s a balance. The harder we make it for bots to access a website, the more we turn away regular humans as well. Here s a short and non-exhaustive list of techinques: User Agent Filtering CAPTCHA solving Rate Limiting Proof of work Identification Paywall User Agent Filtering When a person/bot requests a page from a website, the HTTP header of the request has a field called User-Agent . This is to denote the type of client that the requester is using. For example, when I visited a website just now, I sent the user agent Mozilla/5.0 (X11
Exploring via Public Transit
Jun 15, 2025 · original
Last weekend, on my way back north from visiting downtown, I took a break near the Crestview lightrail station. There, I had a wonderful meal at the Kura revolving sushi bar . Afterwards, I walked around the Kinokuniya Bookstore . Honestly, this spot is not something I would ve naturally discovered on my own. Using public transportation is a great way to explore the neighborhoods around you. Busses often don t take highways, and instead will take you through areas that you would ve otherwise skipped. You can find many great restaurants to eat in the Bay Area right next to the Mountain View Caltrain station. A few years ago when Clare and I visited Portland, Maine, we got to explore the thousand islands by a mail boat . Even if you have a car, it s worth taking a look at the transit maps to see if there are any hidden gems.
Embrace the Heat
Jun 8, 2025 · original
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. I don t currently have a car so I rely on public transportation and walking to get around. As such, I m consistently exposed to the heat. On the weekends, there is a strong temptation to hunker down and enjoy my air-conditioned apartment. However, the part of me that loves going out and exploring wins in the end. As with any outdoor adventure, it s always important to be prepared. I don t leave my apartment without the following three items: bucket hat, sunglasses, and a water pack. Out of these, I would say the most important is drinking lots of water. It s the best way to regulate body temperature after all. Also, it s better to start your day early, before the temperatures climb. Even after the sun goes down, it takes
Verifying Proofs with Type Checkers
May 27, 2025 · original
The Curry-Howard Correspondance establishes a direct connection between computer programs and mathematical proofs. Programs Proofs Type Formula Term Proof Type has an element Formula is provable Type does not have an element Formula is not provable When we think about traditional type systems, however, most are uncapable of expressing interesting formula. This ultimately limits the formulas we can prove. For example, consider the simply typed lambda calculus. In that system we have base types like int and bool , as well as function types $t1 \rightarrow t2$ which take a type and return a type. From that system, we can then create a proof of an integer by showing the term 0 . The following shows how to use the Lean 4 type checker to verify that 0 is an integer: #check (0: Int) This, however, isn t a very interesting proof or formula. What would be more interesting is if we can use a type
Is this program safe? Lessons from Type Theory
May 10, 2025 · original
This blog post is inspired from a lecture that Dr. Ana Milanova gave in her Principles of Program Analysis course. Consider an arbitrary computer program. When we execute it, we expect that it will produce some result and not get stuck . For example, id = lambda x: x id 5 In the code above, we create an identity function id which takes an argument x and returns that same argument. Therefore, in the second line when we call the function with the value 5 , we receive the value 5 as a result. Now what about the following? 5 id This program does not make any sense since the value 5 is not a function and hence does not take anything as an argument. Ideally, we want to catch errors like these before we run our code. In fact, we can by relying on a type checker . Through this, we only execute programs that have a valid type . If not, then we say that the program is invalid. id 5 is of type int

Discovered by the rss-feed-index crawler, which checks each feed at most once a month.

Same record as JSON: https://api.agentalog.com/api/feeds/fd_brandonrozek_com_8d40b3c02243c8be. More from this site: brandonrozek.com in the Feeds tab.