28.3922° N // 80.6077° W — Cape Canaveral Range

One coastline,
many trajectories.

Ramblings from Florida's Space Coast — across systems security, formal mathematics, orbital mechanics, synthetic biology, and the tools in between. Eight payloads, one launch site.

Range schedule

Next off the Cape

Upcoming launches from Cape Canaveral & Kennedy Space Center, pulled live from The Space Devs' Launch Library.

Acquiring range telemetry…

Data: Launch Library 2 · thespacedevs.com

Manifest

Trajectories under track

Each area is its own orbit — different regime, different math, but launched from the same place and reasoned about with the same tools. Designators encode the domain, not a ranking.

SEC TRK 01

Security of VMs & Containers

Hardening the boundary between guest and host: hypervisor escapes, namespace and cgroup isolation, seccomp/eBPF policy, sandboxes like gVisor and Kata, and the supply chain that ships into your images.

hypervisor isolationseccomp / eBPFgVisor · Kataimage supply chain
1 log
NVM TRK 02

Neovim

Building a keyboard-native editing environment from Lua up: LSP, Treesitter, tuned motions, and the small ergonomic decisions that compound over a decade at the terminal.

Lua configLSP · Treesittermodal ergonomicsplugin surgery
No logs yet
AI TRK 03

Artificial Intelligence

LLMs as reasoning substrates, multi-agent swarms and the emergent behavior they produce collectively, and the ML foundations underneath. Where individual agents are simple and the group is not.

LLMsswarm intelligenceemergenceML foundations
No logs yet
CAT TRK 04

Category Theory

The algebra of composition that quietly underlies everything else here: functors, natural transformations, adjunctions, and monads — structure that lets ideas move between fields without losing their shape.

functorsadjunctionsmonads(co)limits
1 log
PRF TRK 05

Lean & Rocq

Machine-checked mathematics with dependent types. Writing proofs a computer will actually verify, chasing tactic automation, and treating correctness as something you compile rather than hope for.

dependent typesLean 4Rocq / Coqproof automation
No logs yet
ORB TRK 06

Aerospace · Low Orbit

Orbital mechanics for LEO: injection, decay, station-keeping, and rendezvous. Watched from the coastline it launched from — reasoning about the cadence of the Cape and the smallsats it lofts.

LEO dynamicsorbit determinationlaunch cadencesmallsats
No logs yet
GEN TRK 07

Genetic Engineering

Toward programming languages for the genetic engineering of living cells: cells as a programmable substrate, genetic circuits as compiled logic, and DSLs that let you write a phenotype and lower it to DNA.

cells as substrategenetic circuitsDNA compilationsynthesis DSLs
1 log
RTR TRK 08

Retro PC Gaming

The DOS-and-early-Windows era and the craft of keeping it runnable: preservation, emulation, sound-card archaeology, and the demoscene that pushed those machines past spec.

DOS-era PCpreservationemulationdemoscene
No logs yet
STR TRK 09

AI Gen Notes

These are research docs, notes, and etc. That have been generated by generated via AI.

StartupsLLMsFormal MethodsmathematicsAI/MLPhysics
2 logs
Ground station

About this site

spacecoast.dev is a working notebook for someone who refuses to pick a single lane. The through-line isn't a topic — it's a method: build the boundary carefully, prove what you can, and treat living cells, virtual machines, and orbits as systems you can reason about precisely.

Category theory is the connective tissue; Lean and Rocq are where the arguments get checked; the Cape is out the window. Expect deep dives, half-finished experiments, and the occasional retro machine brought back from the dead.

Station keeping

Site
spacecoast.dev
Locale
Space Coast, FL
Payloads
9 active
Editor
Neovim
Provers
Lean 4 · Rocq
Status
Range green