I guess I can file compcert as another example of "lofty promises of formal verification don't always match reality" https://lobste.rs/s/qlrh1u/runtime_error_formally_verified …pic.twitter.com/e0HDiUWA8l
You can add location information to your Tweets, such as your city or precise location, from the web and via third-party applications. You always have the option to delete your Tweet location history. Learn more
It seems like formally verifying their conversion from source to AST should be the low-hanging fruit. Did they just find it to uninteresting to do?