“Does this program compute this function?” is a hard problem — unsolvable.
“Is this a proof that this program computes this function?” is an easy problem — primitive recursive in any reasonable encoding scheme, maybe of near-linear complexity.
Both of these might be described as “verification”.
“Verification” is also vague.
“Does this program compute this function?” is a hard problem — unsolvable.
“Is this a proof that this program computes this function?” is an easy problem — primitive recursive in any reasonable encoding scheme, maybe of near-linear complexity.
Both of these might be described as “verification”.