Part of the reason SQLite is so prolific is because of the language used, not in spite of it. It’s enabled people to run SQLite on a broad range of hardware, device types and called from any language that supports native C calls (which is a massive array of languages). And let’s not forget the truly amazing performance you get from SQLite too.

Had SQLite been written in a language that would have made it easier to perform a proof of correctness then it wouldn’t be nearly as widely used and because of that language choice and then it likely wouldn’t have had the resources (financial nor community input) to complete a proof anyway. So would it have actually been any less buggy if it weren’t a C project?

Sometimes worse is better and moaning about “what if” is neither constructive nor even warranted when you consider just how well written SQLite already is and how abundant the tests are.