> Known constraints like guaranteed to terminate is useful.

"Guaranteed to terminate" actually means "guaranteed to terminate in finite but possibly arbitrarily large time" which is really not a useful property.

There's no practical difference between a filter that might take 1 billion years to run and one that might take more than a billion years.