~/Blog

Deterministically Iterating over a set within Dafny functions

#Formal Methods

Dealing with Web Scrapers

Exploring via Public Transit

Embrace the Heat

Verifying Proofs with Type Checkers

#Formal Methods

Is this program safe? Lessons from Type Theory

Filesystem as a persistent key-value store in Python

Quick Lean: if-then-else statement in hypothesis

#Formal Methods

10 Years

Recently: April Showers Bring...

Setting up Ollama with CUDA on Podman Quadlets

Weather Forcecasts on the Command-Line with the National Weather Service API

Adventures in Rust WebAssembly

#Rust #Web

Blog Question Challenge (Jan 2025)

Hashing Based on Word (Emoji?) Lists

Naive Encodings of Transitivity within First-Order Logic

#Logic

Rolling out my own CDN with GeoDNS

Curl-able Business Cards

Temporary Port Forward using UPnP in Linux

Listing Offline Pages with Service Workers

Linting my blog posts with Vale

Please monitor disk usage

Introduction to Possibility Theory

Introduction to Dempster-Shafer Theory

Replacing a drive in Btrfs

Monitoring my Hard Drives with SMART Attributes

Process JSON in the terminal with jq

Importing External Schemas in Prost

Hunter-Gatherer Traditions: Apple Picking

Webhook notifications on systemd service failure

Writing Unit Tests in Lean 4

#Formal Methods

Polymorphic Functions w/ Wildcard Matching in Lean 4

#Formal Methods

Modifying JSON in Rust

#Rust

Accessing Homelab Services Remotely with mTLS

Re: Static+, can it work?

Quick Beamer: Generating a slide at the beginning of each section

#LaTex

Recently (June 2024)

Constraints and Safety in PDDL

#Automated Planning

Creating Patch Files

Learning a new language

Migrating from Docker Compose for Podman to Quadlets

Circling around Vancouver

USPS Forever Stamps

Tracking Software Releases via RSS

Disjunctive Goals in PDDL

#Automated Planning

Functions and Inductive Propositions in Lean 4

#Formal Methods

Disabling CPUs to Save Power

Working with integer sets in Lean 4

#Formal Methods

Coercing Ints to Nats for Induction in Lean 4

#Formal Methods

Lean 4 Tutorial

#Formal Methods

Caching Theorem Prover Results

#Logic

SVG Pixel Art

Quick Python: Refactoring Exceptions with Context Manager

#Python

Mapping the states I visited

Wordguess: A game for the Tildeverse

Ice Hockey

Marshalling Python Dataclasses

#Python

Ascii Towns in the Tildeverse with Cadastre

Python Dataclasses: Derived Fields and Validation

#Python

Fun with Telnet

How to get a RSS Feed of your Wikipedia Watchlist

Run a command when a file in a directory changes

Bash Traps: Exit, Error, Sigint

#Bash

No Response Default in Nginx

#Nginx

Switching to Raid 10

#Storage

Renewing my GPG Keys

#GPG/PGP

Starbound Server using LXC

Setting up unprivileged containers with LXC on Fedora 38

#Containers

Adding badges to my website

Re: On Earbuds

Mirror Public Repositories

#Git #Archive

Changing /etc/hosts based on network connection

Simple Key-Value Store using Sqlite3

#DB

Transcoding Plex Video in RAM

Figuring out which git repositories are ahead or behind

#Git

Quickly configuring and testing the Mosquitto MQTT broker

Emoji Kitchen: Combinations of Emojis

Obtaining a IPv6 Address via Hurricane Electric's Tunnel Broker Service

#Networking

Hiding Answers in Lecture Slides using Latex Beamer

#LaTex

Use block storage for your application data

How to set up a private Syncthing network

A day in Brooklyn

#Life

Limiting MongoDB Resource Usage within Docker Compose

#Containers

How to Safely Remove a DNF Repository

#Fedora

Type Checking Javascript Files Using Typescript

#JS

Representing Uncertainty under the Closed World Assumption

#Logic #Automated Planning

Obtaining Valid SSL Certificates within an Internal LAN

Using the DNS-01 Challenge to obtain a wildcard certificate on Letsecnrypt

Progressive Enhancement of Page Transitions in Hugo with htmx

Proactive Defederation, is it worth it?

Adventures in Bird Watching

#Life

Photograph the Ordinary Times

Rebalancing Portfolios: The buy low sell high of investing

#Finance

Diversified Investing using Index Funds

#Finance

Functional Completeness

#Logic

AI fearmongering for regulatory moats

Top 7 Attacks to My Website

The Usefulness of Website Analytics for Personal Websites

Syndicating Hugo Posts to Medium

#Hugo

Avoid Mutating Items within a Set (Python Edition)

#Python

Why pay for things when you can get it for free?

Bonds and Interest Rate Risk

#Finance

Contributing to OpenStreetMap

Tildeverse

Load Balancing within OpenMP Static Schedules

Lean 3 Tutorial

#Formal Methods

Prenex Normal Form - Implication Exercise

#Logic

Induction in Lean 3: Three Techniques

#Formal Methods

Readable Lean 3 Proofs

#Formal Methods

Deploying a Lightweight Git Server with CGit using Docker-Compose

#Git

Bmaptool: A simpler way to copy ISOs

Decentralized PGP Keys with WKD

#GPG/PGP

Decentralized Identities with PGP Annotations and Keyoxide

#GPG/PGP

Obtaining Multiple Solutions Z3

#Formal Methods

Mastodon/Webfinger Alias using HTTP Redirects

#Mastodon

Personal Web Archive and How I Archive Single Web pages

#Archive

Concatenating PDF files in Linux

Blogroll From Subscriptions

#Blogging

Capturing Quoted Strings in Sed

Drawing Trees in LaTex with Tikz

#LaTex

Deploying my Hugo Website through GitHub Actions

#Hugo

Pretty RSS Feeds

#Blogging

The Promise of Decentralized Currency and the Issues with Custodians

Visualizing Nginx logs with GoAccess

#Nginx

Quick Python: Check Submodule Load

#Python

Immutable Traversals with Unfold

#Functional Programming #Scala

Memoization in Scala

#Scala

Corecursion, Unfold and Infinite Sequences

#Scala #Functional Programming

Deep Recursion in Functional Programming

#Scala #Functional Programming

Different Views of Fold and Their Combinations

#Scala #Functional Programming

Fold Not Only Reduces

#Functional Programming #Scala #Haskell

Speaker Notes in LaTex Beamer

#LaTex

Optionality and Risk in Decision Making

Explaining the Shift in Values

Accidentally Reinforcing Model Predictions in iNaturalist with Seek

Identifying Plants With iNaturalist

Getting Podman and Nginx TCPv6 and HTTP/2 Ready

#Networking #Containers #Nginx

How to trim a video using FFMPEG

#Audio-Video

Website Status Checking

Quick LaTex: Footnotes with no Counter

#LaTex

Retreiving GPS data in decimal format from EXIF data in photos

#GPS

Conditional Assignment in Bash

#Bash

Having your Website Visible on the Fediverse

#Mastodon

Git Pushing to Multiple Remotes

#Git

Displaying Hikes with gpx.studio

#Hugo #GPS

Archiving Toots

#Hugo #Mastodon #Archive

Displaying a Toot in Hugo

#Hugo #Mastodon

Hiding Section From Listing in Hugo

#Hugo

Document Formats and Plaintext

#Documentation

On Writing Simple Scripts

Python Argument Parser

#Python

Most Common Mistake in Induction Proofs

#Math

Automatically Updating Podman Containers

#Linux #Containers

Recently (May 2022)

Finding Cool People on Mastodon

#Mastodon

Why I PESOS From Mastodon

#Mastodon

Which commit broke the build? Using Git Bisect

#Git

OpenMPI on Fedora

#Fedora

Rclone: The Swiss Army Knife of Cloud Storage

#Backup

Permission Denied: Writing to Privileged Locations

Networkx Random Sample Graph

#Python

Non-Root Systemd Scripts

#Linux

Finding Cuda Errors

Intensional Logic Extends First Order

#Logic

JUnit Script

#Java

Loop Invariants

#Formal Methods

Git Partial Clones

#Git

Reasoning through Loops in Dafny

#Formal Methods

Program Verification with Hoare Logic and Dafny

#Formal Methods

Docker Secrets

#Containers

Mount Object Storage Locally using S3 Fuse

#Storage

Git Diff by Words

#Git

Aliases for Snaps and Flatpaks

#Linux

Reducing Network Bandwidth in Nginx with Gzip

#Nginx

Dafny v3.3 Show Countermodel

#Formal Methods

Rebuild Kernel Modules with Akmods

#Linux #Fedora

Rootless Docker-Compose with Podman

#Containers

Code alongside Output in LaTex

#LaTex

Multi-Column slides in Beamer

#LaTex

Code in LaTex Beamer

#LaTex

Terminal Output To SVG Animations

LaTex List Labels

#LaTex

Configuring a SOCKS5 Proxy

#Networking #SSH

Tree-based Plots in NetworkX

#Python

Common Network Debugging Commands

#Networking

Lean 3 Theorem Prover Tactics

#Formal Methods

Convert DJVU to PDF

Do-While Loop in Other Languages

Antenna Basics

#Amateur Radio

Parallel SCP with LFTP

Forward Packets with Socat

#Networking

Terminal Output in Vim

Netboot.xyz Bootloader

Ventoy for managing ISOs on one USB

#Virtualization

Comparator Logic Gate

Z3 Constraint solving

Print Statements with Frame Information

#Testing

Introduction to RF Power Amplifiers

#Amateur Radio

Human Readable Sizes

Detect Python Version

#Python

Stow Version Manager

Clearing Systemd Logs

#Linux

LibreOffice Calc Tips

DHCP for Raspberry Pi

#Networking

Quick Bash: Validate IP Address

#Bash #Networking

Quick Bash: Check Argument Count

#Bash

Mirroring with Gitea

#Archive

Mirror a Hugo Site

#Archive #Hugo

Autostart Desktop Applications

#Linux

Chroot and Virtual Filesystems

#Linux

Streaming PulseAudio over RTP

#Audio-Video

Multicast Receive Script

#Linux #Networking

Custom Device Paths with UDEV rules

#Linux

Forwarding Phone's GPS

#GPS

Getting Started with FM Digital Modes

#Amateur Radio

Preserving Classic URLs on my Website

C++ within Python with SWIG

#Python #C++

Quickly Creating CGroups to Limit CPU/Memory of Applications

#Linux

Bandwidth Limiting Applications

#Linux #Networking

Deploying Binaries to other Linux Distros using Appimage

#Packaging #Linux

Reverse One-Hot Encode

#Python

Tail Call Optimization in Python

#Python

Manage Python Applications

#Python

Auto Purge Old Docker Images

#Containers

Creating QR Codes from the Terminal

Launch Apps through the Terminal

#Linux

Partial Argument Parse and Passing in Bash

#Bash

Ignore graphical applications with Xvfb

#X11

Splitting Files to Circumvent Size Limits

Starting Graphical Applications Remotely without X-Forwarding

#Linux #SSH

How to get list of IP Addresses in Python

#Python #Networking

Jupyter with Pyenv

#Python

Quick Python: Async Callbacks

#Python

Firefox Privacy Configuration

GPG Agent as SSH Agent

#SSH #GPG/PGP

Extract All the Things

#Linux

Quick Python: Export Decorator

#Python

PDF To Kindle

GPG Card

#GPG/PGP

SSH Connection Sharing

#SSH

Docker Macvlan Networks

#Containers

How to Drop Commits in Git

#Git

Using OBS as a Webcam Source

#Audio-Video

Loopback Webcam Device with V4l2

#Audio-Video

Configuring DHCP DNS in Pihole

#Networking

Wildcard Domains in PiHole

#Networking

TCP/UDP with Bash

#Bash #Networking

Git Credential Store

#Git

Algorithms in LaTex

#LaTex

Show Applications using the Internet

#Linux #Networking

Git Line Endings

#Git

Auto-Deploy Docker Applications

#Containers

Shared Packer & Terraform Config

#Deployment

Automatic Deployments with Terraform

#Deployment

Snapshot Creation with Packer

Digital Ocean API

#Deployment

Quick Python: __all__

#Python

Python Packaging: Optional Dependencies

#Python

Generate Secure Passphrases Locally with Diceware

#Security

Code in LaTex

#LaTex

OpenVPN Container

#Containers

Quick and Dirty DEB/RPM with Checkinstall

#Packaging #Linux

Replace Audio in Video

#Audio-Video

Quick Python: Cached Property

#Python

Quick Python: HTTP Server

#Python

Quick CA for internal LAN

#Networking #Security

Python Patterns: Subscribe

#Python

Download Changes

Iteratively Read CSV

#Python

Quick Python: Concurrent Futures

#Python

Pip Editable

#Python

Signing Commits

#Git #GPG/PGP

GPG Keygen

#GPG/PGP

Pip Config

#Python

Simple Async in Python with Gevent

#Python

Python asyncio

#Python

Quick Python: Dataclasses

#Python

Quick Python: Copy Decorator

#Python

Quick Python: Getters and Setters

#Python

Quick Python: Unit Testing

#Python #Testing

Quick Python: Decorators

#Python

Quick Python: Memoization

#Python

Birthday Music

#Music

Disc Golf and PyMC3

#Python #Statistics

Quick Python: Length of Iterables

#Python

Pyenv Build Flags

#Python

Uninstall Vim Plugins

Neovim Plugins

Sphinx & MathJax

#Documentation #Python #LaTex

Sharing Patches in Git

#Git

Sharing Specific Commits with Git Bundle

#Git

QTcpSocket

#C++

Qt Timers

#C++

Python Operator Overloads

#Python

C++ Overloads

#C++

Record Output Audio via Terminal

#Linux #Audio-Video

Text to Speech on Linux with Espeak

Dbcli

#Python #DB

Resuming Stopped Apt Updates

#Ubuntu #Linux

Python: Set Interval

#Python

Python setup.py develop

#Python

Automate Python Test Suites with Tox

#Python #Testing

Testing your Python Application on Multiple Versions with Pyenv and Tox

#Python #Testing

Backing Up YouTube Content

#Archive

Quick Python: List Files Recursively

#Python

GStreamer

#Audio-Video

Missing Libraries

#Linux

Quick Python: Package Namespacing

#Python

Custom Executables

#Linux

SSH Jump

#SSH

Find Devices on your Network with a Ping Scan

#Linux #Networking

Bat is cat with syntax highlighting

#Linux

Quick Python: Abstract Classes

#Python

Count Lines of Code (cloc)

Quick Python: Interrupts

#Python

Zsh and Snaps

#Linux

Offline Pip Packages

#Python #Archive

Temporary Static IP

#Linux #Networking

Mirror Download with wget

#Linux #Archive

Burning ISOs with dd/pv

#Linux

Managing Python Versions with Pyenv

#Python

Limit Bandwidth through Terminal

#Linux #Networking

Persistent remote X sessions with xpra

#X11

Balance files across multiple disks using MergerFS

#Linux #Storage

Python Path Hacks

#Python

Cryptographic Games

#Security

Playing with Live CDs

#Virtualization

Quickly Setting up a Storage Device

#Linux #Storage

Control an Android Device Remotely using Scrcpy

Toggling X Input

#Linux #X11

Playing with Filesystems using Virtual Disks

#Linux #Storage

Temporarily Resolving Hostnames

#Linux #Networking

LXD on tmpfs

#Linux #Storage #Containers

Theorem Proving Definitions

#Formal Methods

Analyzing Startup Times with Systemd

#Linux

Advanced Docker Image Construction with Bash

#Linux #Containers

Nested X Sessions with Xephyr

#X11

Ensuring Docker Compose Startup with Systemd

#Linux #Containers

How to use Nginx under Traefik

#Nginx

Setting up coredns and Zone Files

#Linux #Networking #Containers

Spell check on the Terminal with aspell

#Linux

RSA Cryptography

#Security

Simplifying the Definition of Algebraic Groups

#Math

Transforming Videos into GIFs for Slides

#Audio-Video

Collaborating on Beamer Pandoc Slides

Wormhole: Easiest way to transfer files between two linux machines

#Linux

Ngrok

#Networking

Wireguard VPN

#Networking

Man Pages with Pandoc

#Documentation

Blog Workflow

#Hugo #Blogging

Python Typing

#Python

Useful Abstract Definitions

#Math

Custom Python REPL

#Python

Git Lens: Superpower Git within VSCode

#Git

NotImplemented in Python

#Python

Live Documentation

#Documentation

Chirp

#Linux #Amateur Radio

SSH Config

#SSH

Robustly copying ISOs using dd

#Linux

Getting started with Digital Modes in Linux

#Amateur Radio

Shutdown After Job

#Linux

Local Repo From Live Installer

Network Throughput Testing

#Linux #Networking

Virtualizing Environments with Clonezilla

#Virtualization

Systemd with Python environments

#Linux #Python

Parsing CLI Flags in Bash

#Bash

SSH Local Port Forwarding

#SSH

Mirroring or Archiving an Entire Website

#Archive

Copy to RAM Please

#Linux

Memory Errors in Go

Oh My Zsh

#Linux

YubiKey

#Security

Rsync with a Different Key

Simulators

Discovering Ham Radio

#Amateur Radio

Gitlab CI/CD

Handling Background Processes in Bash

#Bash

Why ZeroMQ

#Networking

Debugging and Performance

#Testing

Linux Desktop Icons

#Linux

Custom System Fonts

#Ubuntu #Linux

Unattended Upgrades

#Linux #Ubuntu

VNC Setup

Wacom and USB Redirection in Virtual Machines

#Linux #Virtualization

External Media Formats

#Storage

Capture The Flag

#Security

Symmetric Groups in Python

#Math #Python

Color Manipulation with Sass

#Web #CSS

Python Virtual Environments

#Python

Borg Backup

#Backup

Notes on '13 Ways Designers Screw Up Client Presentations'

Real Analysis Sequences in Haskell

#Math #Haskell

Identifying Misspelled Words in your Dataset with Hunspell

Obtaining Command Line Input in Java

#Java

Escape Sequences in Java

#Java

Albuquerque Real Estate Multiple Regression model

#Statistics

Java Swing Components

#Java

Using System Themes In Java Swing

#Java

Viewing Java Applets

#Java

Male vs Female Life Expectancy

#Statistics

Approximate Pi using a Monte Carlo Simulation

#Math #Java

Simplifying Expressions with Octave

Uniformity of Math.random()

#Statistics

Knit a Document in RStudio

#R

Pass the password manager

#Security

Creating vCards from h-cards

#Web

Playing with QR Codes

Limiting the Cache in Service Workers Revisited

#Web #JS

Math with Fractions.js

#JS

An Offline Experience with Service Workers

#Web #JS

Functions in Javascript

#Web #JS

Javascript Conditional Statements

#Web #JS

Animatable: Transform

#Web #CSS

Animatable: Visual

#Web #CSS

Javascript Data Types

#Web #JS

HTML, CSS, Javascript, and how they all link together

#Web

Animatable: Location

#Web #CSS

Animatable: Text

#Web #CSS

Animatable: Box Model

#Web #CSS

Animatable: Border

#Web #CSS

Responsive Layout and Animation

#Web #CSS

Math Theory for Function Between Two Points