Pure annotation for stateless functions

language design
42

Yes, if we have an explicit side effect between the calls, then we can not reorder the functions. I was talking only about a sequence of function calls which are "pure, but may contain panics". In other words, I was implying the following modification of your snippet:

{
  let y = g();
  let x = f();
  (x, y)
}

IIUC currently the compiler can not reorder f and g, which are potentially panicking, but do not contain any other side effects. Here is a somewhat practical example which demonstrates horrible codegen caused (IIUC) by the inability to reorder panics (uncomment the asserts to see the difference):

Unfortunately, I don't think it can be done in a practical fashion. We effectively have to commit into code a formally verifiable proof that all panics can be removed for the given function. Doing it manually is extremely annoying and time consuming. It's simply impractical outside of very limited high assurance areas. Maybe we could ask the compiler to generate the proof for us, save it into a separate file, and reference it (and re-generate it on each code change), but development of such tooling would require a lot of work with a plethora of open questions.

2 Likes