Brandon’s Pet Server

What lives here

This page is being served by my home server, nousowl. I run the parts of my online life here that make more sense on my own hardware. This box is a playground for learning and for hosting whatever catches my interest.

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 one of many theorem-provers, but which is attractive to me because of work that’s already been done with it in deontic logic, e.g., here. Like Carnap, it takes a bit of configuration on any machine you want to use it on (although it is definitely more straightforward), and it doesn’t work on things like iPads, phones, etc. A dedicated server for this would allow quite a bit of personal freedom on this front. The simple solution is to simply use Isabelle/HOL in the shell on the server (although it’s not very fun to use in the shell). The more complex idea is to actually serve jEdit as a web application with only a scratch buffer, which I can simply access via URL and paste my working Isabelle 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.