The theorem reminds me of William Lawvere's "Adjointness in foundations". Formulas/programs are in an adjoint relationship with their executions. The fact that they are adjoints is a big deal.