On Thu, Jun 9, 2022 at 12:39 PM Greg Stark <stark@mit.edu> wrote:
> Generally I think the idea is that the user *is* responsible for
> writing immutable functions carefully to hide any non-deterministic
> behaviour from the code they're calling. But that does raise the
> question of why to focus on search_path.
>
> I guess I'm just saying my goal isn't to *prove* the code is correct.
> The user is still responsible for asserting it's correct. I just want
> to detect cases where I can prove (or at least show it's likely that)
> it's *not* correct.
Right. It's virtually impossible to prove that, for many reasons, so
the final responsibility must lie with the user-defined code.
Presumably there is still significant value in detecting cases where
some user-defined code provably does the wrong thing. Especially by
targeting mistakes that experience has shown are relatively common.
That's what the search_path case seems like to me.
If somebody else wants to write another patch that adds on that,
great. If not, then having this much still seems useful.
--
Peter Geoghegan