On Thu, Jun 9, 2022 at 12:39 PM Greg Stark <st...@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
