Donald Hobson comments on Use-cases for computations, other than running them?

[Donald Hobson]

Consider this function

$\text{def foo():}\text{a=0.0}\text{for i in range(10**100)}\text{a=a+1/i}\text{return a>2}$

This is valid code that returns True.

Note that you can tell it returns true without doing ${10}^{100}$ operations, and a good compiler could too.

Shouldn’t this also be valid code?

$\text{def foo():}\text{a=0.0}\text{for i in range(}\infty \text{)}\text{a=a+1/(i**2)}\text{return a>1}$

There are a whole space of “programs” that cant be computed directly, but can still be reasoned about. Computing directly is a subset of reasoning.