I've generally liked classic approaches which had entry and exit conditions, and loop invariants, all written using the same syntax and operators as the program. The compiler has to know what to ignore, of course. The compiler should syntax and type check all the proof information, even if it can't verify it. It's important to avoid an impedance mismatch between the proof system and the programming language. If programmers are constantly translating between two notations, customer resistance will be high.

If you need to write functions as scaffolding for proofs, they should be written in the programming language. You might need some operators that aren't actually runnable, such as FORALL, but the syntax should be that of the programming language. If your specs look like

    Γ, P || Q, P ==> R, Q ==> R ⊢ R

in a language with none of those operators, you're doing it wrong. That's the disease of falling in love with the formalism.

The user should not have to tell the proof system things the compiler already knows. Whatever overloading and aliasing rules the language enforces should be known and handled in verification, too. We worked off the syntax tree produced by a compiler front end modified to handle the verification statements, not the raw source code. Ada Spark has different aliasing rules than Ada, for example.

One big problem is that object oriented programming came and went in popularity. You really want object invariants. You need some way to attach an invariant to a data structure. You also need a clear boundary where control enters and exits the objects. If the language doesn't have objects, you struggle with trying to express object type invariants in the proof language. You don't get the boundaries as part of the programming language.

A useful interface between the prover and the program is simply to use

    assert(A);
    assert(B);

in the middle of code to encapsulate complex proof goals. A should be provable from the preceding code using a SAT solver. B, when assumed true, should provide enough info for a SAT solver to proceed from that point. Now you need to prove

    A implies B

by external means. That creates a well defined problem which can be given to something AI-like, backed by a proof checker, to chew on.

Ada Spark has some features that violate these rules. Also, it's hard to find anything about Ada Spark newer than ten years old.

There's a fair amount of interest in verifying Rust. There's been some progress using Dafny. But "Dafny is not Rust. Using Dafny requires porting algorithms of interest from Rust to Dafny. This port can miss details and introduce errors." There's the impedance mismatch again. Verus looks more promising. It is more Rust-like in syntax, they get the SAT solver/AI prover distinction, and there's active development.