Brandon Rozek is a Computer Scientist often writing about topics surrounding Linux and Software Development.
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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.…
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$…
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…
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: set<string>, acc: seq<string>): seq<string> { if collection == {} then…
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…
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.…
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…
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…
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 first level within the five levels of configuration languages is a string in a file. The example that Andreas gives in his blog post is enabling/disabling energy aware scheduling in the kernel. # Read the current value cat /proc/sys/kernel/sched_energy_aware This approach does not require using any custom serializers or deserializers. Instead, the user or program only needs to navigate and…
When verifying proofs about code, I often end up with a hypothesis that has an if statement in it. Depending on how long it’s been since I last used Lean, I forget how to deal with it. This is a quick post to remind me how. Example: example (b: Bool) (n: Nat) (H1: if b then (n = 5) else (n = 3)) : n > 0 := by sorry We want to show that for an arbitrary boolean and natural number n , that n…
On April 16 2015, I wrote my first two blog posts on creating responsive layouts in CSS. It’s crazy to think that I still have this blog going after 10 years. Since then I’ve lived in 9 different places, worked at 6 different organizations, and got to meet many wonderful people including my now fiance. I thought it would be nice to look back over the last ten years, and talk about my…
I woke up this morning to a small layer of snow outside. In the Northeastern part of the United States, it’s said that we have 12 seasons . Winter Fool’s Spring Second Winter Spring of Deception Third Winter The Pollening Actual Spring Summer Hell’s Front Porch False Fall Second Summer Actual Fall At the time of this post, we’re at “Third Winter”. I look forward…
Open WebUI provides a nice chat interface for interacting with LLMs over Ollama and OpenAI compatible APIs. Using Ollama , we can self-host many different LLMs that are open-sourced! This post documents the steps that I took in order to get Ollama working with CUDA using my Podman setup. However given how fast Machine Learning projects iterate, I wouldn’t be surprised if these exact steps no…
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 key 1 . We’ll use this resource to write a small bash script which gives today and tomorrow’s weather forecast given a latitude and longitude. My goal is to have a small bash script which I can run in the terminal to get the forecast…
For two years now, my friend and colleague James Oswald has told me to check out WebAssembly . I avoided it all this time because I thought it would be too complicated to get started with. In one of our study sessions, my friends Chris and Ethan both said they wanted to look into it. I have to say, that getting started with WebAssembly is far simpler than I’ve previously imagined and it…
Catching up on my RSS feeds, Ava’s bear blog question challenge has been making the rounds. The last blogging trend I remember going viral was App Defaults inspired by an episode of Hemispheric Views back in November 2023. I felt too awkward last time around to take part, and I wouldn’t have said anything this time either, except that I got tagged by Mark Pitblado . Nothing makes you…
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-Workstation-Live-x86_64-41-1.4.iso The output of the command should match the given checksum. If not, I should assume that I have a fraudulent ISO. 1…
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 of transitivity in first-order logic and goes over a counter-example 1 . Let $G$ be a binary relation that represents whether…
I noticed when looking at my monitoring that accessing my website from Asia takes almost a full second to load. I apologize to all my visitors in that segment of the green orb. Please do write to me to tell me you exist though! I’m always happy to hear from readers of my blog. Why don’t you use Cloudflare? You see friend, I believe in a decentralized web. I want to do my part in not…
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. Especially since the web UI differs between router models. Unfortunately, a common step of hosting a multiplayer game server at home is to set up a port forward. This tells your router to take traffic coming in at a specified external port , and forward it to one of your computer’s internal IP address…
Using web service workers, you can set it up so that visitors have an offline experience with your website. In my original blog post, I wrote about how to cache pages, and how to show them when the visitor lacks an Internet connection, or a special offline page instead. This, however, doesn’t list what pages are cached on their device. Wouldn’t it make sense to show this in the offline…
How do you write good ? For some, the answer is Grammarly. This, however, falls short to me for the following reasons: Needing to rely on some third party service. Seriously, what if I want to draft my blog posts without Internet? Not configurable. Leave me alone, sometimes I like writing my way . Where’s my beautiful terminal application? I use Vale ( GitHub ) a linter for human prose. It…
You know one of the worst errors to deal with on Linux? No space left on device Why? Because recovery becomes really annoying. Depending on your luck, Linux may try to cache to disk even when it’s impossible causing quite a few commands to fail. If you’re already in this situation, the best thing you can do is try to locate files to remove. You can run du -sh * in any given directory…
Possibility theory is a subset of Dempster-Shafer theory (DST). If you’re not already familiar with DST, I recommend you check out my previous blog post since we’ll reuse a lot of the same concepts. In Dempster-Shafer theory we start off with a mass function $m$ which is defined over all subsets of our event space $\Omega$. When approximating $m$, we need to make $2^\Omega$ estimates.…
Imagine sitting by a tree full of birds. You know the tree only has a Yellow Rumped Warbler ($w$), a Northern Cardinal ($c$), and an American Goldfinch ($g$). These birds are respectful in that they don’t call at the same time. You make the following observations of bird calls: $$ obs = w, w, c, g, g, w $$ What’s the probability that we hear a Warbler next assuming the calls are…
The following are the steps that I take to replace a hard drive in Btrfs with a drive of equal capacity or larger. These instructions are mostly taken from Forza’s Wiki which goes into much more depth. Step 1 : Setup a USB with a live image It turns out that with a hard drive missing, my system would refuse to boot. To get around this, we’ll need to use a live image to get to a…
After having a hard drive fail on me once, I’ve been slowly upgrading my homelab to be more resilient. Currently I take daily backups using Restic , push it offsite to two different services, and have 4 hard drives set up in a RAID 10 configuration . The RAID 10 configuration means that I can safely lose one hard drive without needing to access my backups. Though you know the saying,…
The jq command is great for quickly viewing and manipulating JSON data. By default, the output is formatted is a human-readable way, and they provide an easy way to “filter” or access elements within the JSON data. For example echo '{\'firstName\': \'Brandon\', \'lastName\': \'Rozek\'}' | jq Outputs { 'firstName' : 'Brandon' , 'lastName' : 'Rozek' } To see what’s in the field…
Prost is a popular Protocol Buffers implementation written in Rust. The protoc command is commonly used to generate serializers and de-serializers for many different languages. However, the Prost team instead recommends compiling the Protocol Buffers schema directly within build.rs . In this post, I’ll give a quick tutorial on how I compiled my Protocol Buffers schema when I needed to depend…
One of the fun yearly traditions that Clare and I have is to go apple picking. After all, we live in a state that produces a lot of apples . Apple picking season always happen earlier than we expect, with peak season happening in September and October. We went to Windy Hill Orchard and they have the following apples available: Cortland, Empire, Fuji, Gala, Golden Delicious, Janogold, Macoun,…
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. I pray that it’s empty UNIT LOAD ACTIVE SUB DESCRIPTION 0 loaded units listed. Except, I don’t. Instead, I have it set up so that I receive a webhook notification via Zulip whenever a service…
When writing Lean code, it’s easier to iterate with unit tests than to prove properties about the function off the bat. I mean if the unit test doesn’t even pass, why bother with the proof? Luckily, Lean 4 let’s us do unit tests with a cool command called #guard #guard 1 = 1 This checks whether the following expression evaluates to true . Note that this does not provide a proof…
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 := match s with | Sign.pos => (3 : Nat) | Sign.neg => (-3 : Int) The function posOrNegThree depending on the input, can either return an expression of…
For my new role, I’ve been learning Rust. I don’t know why I didn’t learn it earlier, I enjoy it so much that I decided to power my toots page with it. When I query my toots, I receive a JSON response like the following: [{ 'id' : '112581869512127927' , ..., 'content' : '...' ,}, ... ] Some parts of the JSON response changes quite frequently. Since I archive the changes, I want…
One common approach to securely accessing remote services is to use a VPN. This builds an encrypted networking layer which makes it easy to use SSH, HTTPS, and other various protocols. Personally, this worked great on my Linux machines. However, I found it a pain to use on a mobile device. On Android, you can only use one VPN at any given time. This is the case even when the IP ranges are not in…
Gabriel recently released a blog post thinking about the space between a static website and a full-blown CMS. It’s something that I think about semi-often. It’s difficult to characterize what static+ means, because I believe we each have our reasons for using a static site generator. This includes but is not limited to speed , security , and my personal reason of data portability . I…
People want to know where they are within your presentation. This is why for a class of long presentations, there’s an outline slide in the beginning and section headers. Separating sections with an additional slide is nice because it not only gives an audience an opportunity for questions, but it also allows you to sneak in a sip of water. To accomplish this automatically, thanks to a tip…