Is this a mistake in a proof or a mistake in a calculation?
Let's say that the distinction here is how we establish that an answer is correct. A proof is correct if it typechecks (no really). A computation is correct if it faithfully executes the algorithm.
This distinction is more than a little artificial, but in practice it matters a lot.
Let's say that the distinction here is how we establish that an answer is correct. A proof is correct if it typechecks (no really). A computation is correct if it faithfully executes the algorithm.
This distinction is more than a little artificial, but in practice it matters a lot.