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.