← Back to context

Comment by johnisgood

3 months ago

Is it possible to find UB in "unsafe" at compile time?

By using some proof tools, you can find some of it.

It is technically impossible to find 100% of it at compile time because some of the finer details about what is UB are not nailed down 100% yet. But those are generally pretty fine corner cases, and one of the goals of those definitions is to not invalidate code as written.

Formal verification is very hard.