Inch [1] has an example using complexity annotations, showing that a red-black tree insert/delete are linear in the black height. ATS [2] is my go-to language

Inch [1] has an example using complexity annotations, showing that a red-black tree insert/delete are linear in the black height. ATS [2] is my go-to language for static guarantees with C's efficiency. Not sure if it counts as small but the implementation is not big. [1] https://github.com/adamgundry/inch https://github.com/adamgundry/inch [2] http://www.ats-lang.org http://www.ats-lang.org