Comment by rectang

But UTF-8 is also extremely well-studied.

We can have an LLM enumerate all those edge cases, and we can assemble them into a spec. Then we can integrate that spec into a proof.

And because the spec is functional rather than expressive, we can produce copyright-free, provably correct reference implementations whose correctness is as strong as our spec and our proof process.

This reference implementation would then be available for use by a language like PHP, or perhaps an LLM generating a vibe-coded dependency.

Over time, then, the accumulation of such proven reference works grows. We'll never prove all the application code out there correct, but incremental progress is possible.