Stahl in 2020
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.
Overview
Stahl (Language):
- Stahl Core interpreter
- Stahl Core compiler
- Properly grok higher-order pattern unification
- Write Stahl to Stahl Core conversion
- Proper Stahl frontend
- Linux Runtime
- GRIN backend
StahlOS:
- Rewrite/port StahlOS for Pinebook Pro
- Spawn driver and process for serial console on UART
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.)
StahlOS
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).