Five approaches to building a programming language with every known level of type safety (10 levels, from basic types to homotopy types). An exploration mapping the territory of type safety via five concurrent routes (extend, dyadic, aspect, aggregate, clean-slate) sharing a common test suite and documenting all failures in a stumble journal.
programming-language open-source dependent-types language-design compiler-design immutable-types language-comparison homotopy-type-theory research-software idris2 affine-types hyperpolymath epistemic-infrastructure epistemic-computing echo-types choreographic-types veridical-computing type-safety-taxonomy
-
Updated
Sep 21, 2026 - Just