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) and a private Carnap instance, 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, construct counter-models, and translate English into formal notation—all checked in real time in the browser. The core logic library is pure Haskell compiled to JavaScript via GHCJS, so proof checking runs entirely client-side. I use Carnap to teach propositional and first-order logic at UC Davis (PHI 12 and PHI 112) from forall x: Calgary. My instance is live on nousowl here. I build it from source with Nix—GHC for the server, GHCJS for the browser client—and run the resulting Docker image as a container backed by PostgreSQL. Registration is closed for now, but feel free to chat with me if you’d like to figure out a way to interact with it. Day to day I use it mostly for curriculum development: I edit assignment Markdown over SSH and see the rendered interactive exercises immediately in the browser—something like an Overleaf for logic homework. It’s also a way to dig into the Haskell source and understand the whole system from the inside out.

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.

Zulip

Zulip is like Slack but with LaTeX syntax support and better asynchronous threading. For example, a working group like LLEMMMa could benefit from having a dedicated chat server on a UC Davis domain: llemmma dot ucdavis dot edu slash chat. Obviously, like with Carnap, one of the main purposes of this would be to learn about hosting the server; but who knows, perhaps the server becomes a little discussion board for me and my friends.

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). One of the memory sticks is in the process of failing, but I’m leaving the system up in the meantime—nothing I’ve used has broken yet, and I want to see what happens. Everything important is backed up elsewhere.