Comment by rectang
8 hours ago
I just gave this prompt to duck.ai (5.6 Terra under the hood): "How would one go about writing a provably correct algorithm to count UTF-8 code points?"
It gave me something which looked pretty legit. Of course, the generated output very likely to be subtly wrong, but as starting input to a formal checked specification/proof process it seemed like a good start.
I wrote some UTF-8 based string handling software back in the day. It doesn't seem unreasonable to write up a set of requirements and edge cases and then have a formal mechanism prove correctness for common UTF-8 string manipulation operations.
[PEAK HN ON] Now if we could just write provably correct exception handling, we could solve one of the two PHP vulns from today. [PEAK HN OFF]
UTF8 is one nasty little standard. So many edge cases.
I should check it against my email address validator that would be a nice benchmark. It's interesting that there are people that are using email addresses that are not actually valid according to the standard.
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.
I think such constructs should be part of the language or at least of the standard runtime library and not re-implemented by every Tom, Dick, Harriet & HAL.