Skip to content
View andrew-johnson-4's full-sized avatar
🐢
..
🐢
..

Block or report andrew-johnson-4

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Please don't include any personal information such as legal names or email addresses. Maximum 250 characters, markdown supported. This note will be visible to only you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
andrew-johnson-4/README.md

Hi, I'm Andrew Johnson

$$ y^2 = x^3 + ax + b $$

When a program has nothing surprising to say, it should say nothing. — Rule of Silence

Mountains cannot be surmounted except by winding paths. — Johann Wolfgang von Goethe

2025 Roadmap (Working towards a verified kernel language)

If you are considering trying to learn LSTS, please wait until the V3 compiler and v1.0 language standard comes on line. Hopefully this will happen late 2025-early 2026.




Work-Order Priorities

  • FAST Memory-Efficient Compiler (hopefully by the end of 2025-ish)
  • C Frontend to be mostly standards compliant + some common C extensions
  • LSTS to feel like a stable language
    • LSTS has lots of cool features (mission accomplished)
    • now it just needs to soundly and efficiently compile stuff
    • typechecking (full soundness proofs) with some notable exceptions that are theoretically unavoidable
      • template divergence
        • sometimes we can catch this, but in general it is undecidable
      • principle of nominal trust
        • axioms can be frozen, but they can't be removed
        • all good theorem provers have this problem if they allow new axioms to be declared
    • good error messages for all kinds of unsound programs
    • FAST code and compilation speeds (sub 1s self-compilation on Github task runners)
    • standard library makeover
      • linear typesafe pointer management
      • no memory leaks / implicit reference-counted GC
      • some generics to avoid over-specialization
      • benchmarks vs C++, Rust, ML

Upcoming Planned Features

  • Language Standard v1.0
  • Representation Selection for Closures with auto GC
    • oddly enough, this is also a library, not a hardcoded compiler feature

Product Oriented Goals

  • Turn LM into a decent "yak herder" for C programming
    • the goal here is for people to interact meaningfully with C codebases without actually having to touch C

Pinned Loading

  1. Lambda-Mountain-Compiler-Backend/lambda-mountain Lambda-Mountain-Compiler-Backend/lambda-mountain Public

    Compiler Backend for LSTS (Typed Macro Assembler)

    C 33 2

  2. Lambda-Mountain-Compiler-Backend/LSTS Lambda-Mountain-Compiler-Backend/LSTS Public

    Large Scale Type Systems: ML/C Hybrid Programming Language

    124 3

  3. Lambda-Mountain-Compiler-Backend/lsts-language-reference Lambda-Mountain-Compiler-Backend/lsts-language-reference Public

    LSTS Language Reference Website

    HTML 1