Even the trivial specification "given a valid input, the program exits successfully with some arbitrary output" will already get you very far: to prove this trivial specification as correct, you need to prove the absence of panics, undefined behavior or infinite loops. Doing that for a complex program will require formulating useful invariants and proving those. So even if using the trivial specification for the overall program, you'll likely find that the proof will require you to write actually useful specifications for several components of your program (because the program likely contains code that relies on the correctness of the component, in order to prove absence of crashes in the code using the component).
> 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.
