Pavel Stehule <pavel.stehule@gmail.com> writes:
> st 29. 6. 2022 v 6:28 odesílatel Bryn Llewellyn <bryn@yugabyte.com> napsal:
>> Moreover, this "hermetic" property of a to-be-immutable function can be
>> established only by human analysis of the function's source code.
> Our immutable functions are more tolerant than they should be - for real
> immutable functions we should disallow SQL inside functions (and everything
> that is not immutable (plpgsql_check raises warning in this case)), but it
> is allowed.
It's generally believed that Turing's proof of the undecidability of
the halting problem [1] implies that it's impossible to mechanically
prove or refute function properties like immutability. Admittedly,
Turing was concerned with the most general case --- that is, he showed
that *there exist* cases for which no algorithm can give the right
answer, not that any specific practical case can't be proven.
Still, that result has discouraged most people from spending much
time on mechanically checking such things. If you declare a function
immutable, Postgres will believe you; the consequences if you lied
are on your own head.
regards, tom lane
[1] https://en.wikipedia.org/wiki/Halting_problem