Fall 2020 Plans2020-09-04

RIP, 5 month gap.

Short-Term Plans (Next Semester)

• Silver: Finish highlighting, maybe take a look at LSP? Perf still seems problematic, though if the Eclipse plugin's performance is less bad than Monto 3's was, seems like there's still low-hanging fruit.

• Algebraic Effects for ableC: The Koka group recently had a talk on how they compile their language (with algebraic effects) to efficient C. I think the same approach should work to implement an algebraic effects extension for ableC too.

• Stahl eliminators: In theory, I should be able to define a function that recurses over the definition of a datatype to be act as an eliminator/induction principle for it. The original levitation paper defines one, but their formulation doesn't work for the cleaned-up representation for datatypes I'm using (from A Practical Guide to Levitation). I've been toying with a different representation that I hope would make defining the generic eliminator easier, and improve the performance of a naive compiled implementation, so hopefully that works?

Long-Term Plans (Thesis?)

Algebraic Effects in Stahl

I think either linear types (or one of its extensions, such as quantitative type theory) or /maybe/ coinduction might be able to fix the soundness issues? I don't know how to do the proofs of soundness for MLTT (or dependent type theories in general), so I'd need to learn to do those first.

Cubical Levitation

Even if I get the Stahl eliminators item above working, Stahl still won't have everything present in most HoTT/Cubical type theories. The biggest item is higher inductive types (HITs). I don't think these should actually be too incredibly hard to work in, but I don't know what soundness problems exist with HITs, and I should like, actually learn the mathematical model behind cubical type theory.

Formally Verifying StahlOS

The parts of the implementation that (in my opinion at least) it makes sense to formally verify are:

• the builtins, which I'd probably need to define axiomatically in the high-level semantics.
• the "pseudobuiltins", which are basically just hand-compiled code that should be identical (or nearly so) to what the normal compiler would output.
• the first file of the init process, which defines functions, IF, loops, string literals, and a lot of other stuff that would normally be built into the language itself.
• a simple REPL that runs over the serial port.

This notably excludes the serial driver and the bootloader, but I think I'd like to try and verify everything from when the bootloader hands off to the kernel on.

I think this would probably have me learning separation logic, and possibly one of the theorem provers with better support for calling an SMT solver (e.g. Isabelle, though I remember a paper about extending Coq with one).