If you can reduce a proof of a theorem to a finite number of operations, then I'd argue (and you'd agree) that the scheme + program (or just the scheme) is sufficient proof.