Brandon’s Pet Server

What lives here

This page is served by my home server, nousowl—a small, headless Fedora box that holds the parts of my work that belong on my own hardware. It hosts a static site or two (including this one), a private Carnap instance, and a small private Zulip server, and it doubles as my testbed for learning self-hosting by running these systems myself.

Services and plans

Carnap

Carnap is an open-source Haskell framework for formal logic, used to run interactive courseware at dozens of universities: students build Fitch-style proofs, fill in truth tables, and construct counter-models, all checked in real time in the browser. My instance is live at carnap.nousowl.net, built from source with Nix and run as a Docker container backed by PostgreSQL. I teach propositional and first-order logic at UC Davis (PHI 12 and PHI 112) from forall x: Calgary, but this instance isn’t the one my students use—it’s where I write and test course material and tinker with the code itself. Registration is currently closed, but feel free to get in touch if you’d like to figure out a way to interact with it.

Zulip

Zulip is like Slack but with LaTeX syntax support and better asynchronous threading. My instance is live at chat.nousowl.net, self-hosted alongside Carnap behind the same reverse proxy and running as a set of containers with its own PostgreSQL. It’s small and private—invitation only rather than open registration—mostly somewhere for a few collaborators, though part of the motivation is still seeing what a group like LLEMMMa might get out of one.

The following are things I’d like to eventually host on nousowl but haven’t set up yet.

Isabelle/HOL

Isabelle/HOL is the proof assistant behind the computational side of my research. I use it to formalize non‑normal modal and deontic logics—machine-checking how their axioms and semantics correspond, and working toward completeness (an early piece lives here). Work like LogiKEy first drew me to it. Like Carnap, it takes some configuration on each machine and won’t run on an iPad or a phone, so a dedicated instance here would let me reach it from anywhere. The simple version is to run Isabelle in the shell on the server—workable, if not much fun. The more ambitious one is to serve jEdit as a web app with a single scratch buffer, reachable by URL, that I can paste working theories into.

Git hub

Yes, lowercase “h”. Why not make a single machine my everything? I could use RAID to back everything up. I imagine, though, that having such a machine would require more sophisticated hardware than I’m currently using.

System Information

Hardware

Software

Security

Status

The server currently runs a minimal configuration: site hosting behind Caddy, a configured firewall, and automatic updates. I prioritize staying current over maximizing uptime, so the machine may reboot when required for updates (typically during off-hours). A single memory cell turned out to be defective—one 64-bit word, always the same one, found by memtest86+ after a firmware update, and very likely the cause of some unexplained crashes last winter. The kernel now reserves the small region containing it, so nothing is ever allocated there; the rest of the 64 GB is unaffected. Everything important is backed up elsewhere regardless.