Cannot prove some program is correct, in general, because that’s effectively the halting problem. But in practice it is sufficient to enforce (prove) the absence of behaviors via constraints like types or contracts.