$$ 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
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.
- 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
- template divergence
- 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
- cold-start script for collaborative editing LSTS with AI
- Language Standard v1.0
- Full C Support
- Cold-start script so that anyone unfamiliar with LSTS can use an effectively pretrained AI to start collaboratively "vibe coding" in LSTS
- LSTS (and theorem-proving specialized languages in general) are particularly well-suited to work with AI
- the AI can "fail and learn" faster
- the programmer can "oops" more
- etc.
- the development trajectories could then hopefully be more high-level, objective-oriented, product-oriented
- Representation Selection for Closures with auto GC
- oddly enough, this is also a library, not a hardcoded compiler feature
- 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