From reading the docs, one main reason is that they want the output of compilation to be plain C. The Wuffs toolchain source-to-source compiles to plain C source, which can then be compiled and linked anywhere that has a C compiler and/or an FFI to the C ABI, which is a lot of places. Wuffs verifies its safety properties entirely at compile time, so once verified, it can translate the code to completely unchecked C code that is nonetheless known to be safe.