I had not heard of Wuffs (“Wrangling Untrusted File Formats Safely”) before. The language sits at an interesting part of the design space. The type system seems largely oriented around making it safe but fast to manipulate arrays and subsets of arrays, as is commonly needed when decoding media file formats. All the safety checks are done at compile time (either through the type system automatically, or in some case needing programmer assistance to make the proofs go through), which means that once statically proven safe, it’s translated to plain C code without any runtime checks. It avoids some of the problems previous “safe C” dialects have run into by not trying to be a general-purpose language (for example, you can’t dynamically allocate memory).