> to prove this trivial specification as correct, you need to prove the absence of panics, undefined behavior or infinite loops.
Note that Rust supports this already for a significant subset of code, namely 'const fn' code. This is also the subset of Rust that could most feasibly be extended to support something akin to theorem proving since it's supposed to be safely evaluated "at compile time", just like a Coq proof term or script. If Rust had some simple but comprehensive support for raw "proof terms" - namely, expressions evaluated at compile time which could either result in () or abort the build, I assume that much of the "convenience" features involved in an actual theorem prover could be implemented as macros and live in custom crates. But we don't know what a raw "proof term" could look like in Rust for useful program properties.
Note that Rust supports this already for a significant subset of code, namely 'const fn' code. This is also the subset of Rust that could most feasibly be extended to support something akin to theorem proving since it's supposed to be safely evaluated "at compile time", just like a Coq proof term or script. If Rust had some simple but comprehensive support for raw "proof terms" - namely, expressions evaluated at compile time which could either result in () or abort the build, I assume that much of the "convenience" features involved in an actual theorem prover could be implemented as macros and live in custom crates. But we don't know what a raw "proof term" could look like in Rust for useful program properties.