ATS2 has full support for linear and dependent types, capable of operating at pointer-level arithmetics. While the docs may seem impenetrable, in essence it's just a framework of four composable components 1) constrained data types T's, 2) description of resource management and ownership V's, 3) a statically checked "package-deal" (T * V) for lawful programmer-decided ownership semantics (as opposed to "the only true way" in Rust), and 4) formal proofs of the programmed logic. And you are free to mix & match them canteen-style.
Whenever there's a need for complex C API with generics, it's much more pleasant to implement it as a wrapper atop verified ATS C-output rather than C itself.
https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML...
59
14