Correct. You wouldn't prove everything in a typical production system unless that system is controlling a rocket or a pacemaker.

You may want to prove some things. Test others.

Types are proofs by the way. Most programmers find that handy.

I think assertions are rediculously underused BTW