Home Contact Projects

Stahl in 20202020-01-01

This is a quick roadmap for the Stahl project(s) in (at least the beginning of) 2020. I've been slowly reading Homotopy Type Theory over the last week, and I'm getting a Pinebook Pro as a hackable dev platform.


Stahl (Language):


Stahl Core

The Stahl surface syntax is translated down to a simpler intermediate language, Stahl Core. Stahl Core uses an intensional constructive type theory. Currently, I don't think I can make it completely HoTT-friendly, since I'm not sure how to compute with the univalence axiom, but if that changes it probably will be. Lastly, "normal universes" are explicitly indexed with ordinals, which inhabit their own universe, Ordinal.

I'd like to also introduce the tricks from The Gentle Art of Levitation, so its Tag and Desc will likely make an appearance in some form. (Tag, in particular, I'm likely to rename to Atom.)


Since the Pinebook Pro is such a well-documented machine, I want to switch to porting StahlOS to it, rather than continuing to not work on it for amd64. The current codebase is basically blocked on my not wanted to grok ACPI; DeviceTrees seem much saner, and the RK3399 (the SoC the Pinebook Pro uses) looks like it has static addresses for its peripherals (e.g. the serial port is at a fixed physical address of 0xff1a0000).