Thank you. That makes things clearer.

I especially appreciate the trick of asserting the intermediate truth to help the prover along.

As someone who writes software I very much agree that verification of asserts before run time (written in the language itself) is very approachable to a programmer.

In a similar vein I agree with the folks at Jane Street that aiming to rule out specific classes of bugs (as opposed to proving a program is entirely correct) is a very practical goal.