Pavel Stehule <pavel.stehule@xxxxxxxxx> writes: > st 29. 6. 2022 v 6:28 odesílatel Bryn Llewellyn <bryn@xxxxxxxxxxxx> 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