Comment by tialaramex

In fact codecs in particular should be written in something much stricter but more special purpose than Rust, WUFFS (Wrangling Untrusted File Formats Safely)

https://github.com/google/wuffs

WUFFS gives up generality - you can't write "Hello World" in WUFFS because it lacks both strings (for the "Hello, world" text) and I/O (for the printing it out). But you can write a codec, going from a block of bytes representing the encoded file to a block of bytes representing pixels, or PCM audio, or indeed uncompressed data [or vice versa] is easy.

But unlike Rust, all of the safety in WUFFS was checked during compilation. For example Rust emits bounds checks, arr[n] might panic at runtime if n is outside the bounds of arr, but WUFFS doesn't do that, it'll have proved mathematically that n is always in-bounds, if it can't prove that it rejects your code, make sure n is in bounds and try again.

Sometimes the end result is similar, you write code to check n at runtime, if it's a miss you report an error, WUFFS can see you met the criterion - basically the same as Rust. But often in a codec design you can just prove it's in bounds, if you implemented it correctly.