What is a good formal definition of purity?

I like this answer. In particular, it rules out non-terminating programs, which also is a side-effect imo.

Perhaps building on that intuition, a side-effect is any information you get while running a program. A pure program indeed always terminates and there isn’t anything you get to know by running it. Untyped LC has non-termination, so by successfully evaluating an expression you get to know something.

Now, the notion of side-effect you want to observe also depends on how you interact with/instrument your evaluator. Take local state as an example: I consider a function that uses interior mutability as in rust pure as long as that mutability doesn’t leak outside.

You can model such “side effects” entirely as a desugaring to the pure calculus. Your language’s machine implementation might do something smarter. It doesn’t matter, as long as the external observer can’t/decides not to see the difference. By contrast, if the machine has to ask the observer for a new ref cell, for example, that’s when the program is no longer free of side-effects.

I think this is relevant: On the Expressive Power of Programming Languages by Shriram Krishnamurthi [PWLConf 2019] - YouTube

If you can talk about expressive power, you can start defining what you mean by pure. What power must a language have or lack to be pure?

It matches my intuitions better than other formulations. (Thinking about “side effects” is a red herring.)

That’s interesting: I was seeing if there were any slides for Krishnamurthi’s presentation when this appeared:

…is there a connection?