> a mechanism to prove that code can or cannot panic would be great

As appealing as the idea of a #[cfg(nopanic)] enforcement mechanism is, I think linting for panic() is the optimum, actually.

With a more rigidly enforced nopanic guarantee, I worry that some code and coders would start to rely on it (informally, accidentally, or out of ignorance) as a guarantee of completion, not return behavior. And that’s bad; adding language features which can easily be misconstrued to obscure the fact that all programs can terminate at any time is dangerous.

Lints, on the other hand, can be loud and enforced (and tools to recursively lint source-available dependencies exist), but few people mistake them for runtime behavior enforcement.