I would suggest that effects which are "directly" embedded are impure effects (w.r.t. our other thread). Essentially, without reifying them into values with types it's harder to reason about them.

A more interesting dividing line are things like computation effect typing in languages like Bauer and Pretnar's "Eff" or McBride's "Frank".

http://www.eff-lang.org/

http://homepages.inf.ed.ac.uk/slindley/papers/frankly-draft-...

But yes, if you consider other "practical, modern" languages, many retain impurity.

There are very different options.

First, approaches like Eff take pure functional computation as a basis and layer effects like call/cc or concurrency on top of that. I think it's better to go the other way and take concurrency, or, if you want to start sequential, a lambda-calculus with jumps a la call/cc or lambda-mu, as a basis see pure functional computation as a restriction of the base calculus.

Second, it's unclear that effects should be reflected in types for reasoning. That road leads to complicated typing systems without type inferences (see also dependent types). I think the following alternative is more appealing: stick with lightweight types (think Hindley-Milner), and leave reasoning to an external calculus (variants of Hoare logic).

That "analytic" style you suggest is really interesting, too. I'm not sure I have a dog in the ultimate race and I'd love to see both analytic and synthetic styles flourish, but from a mere terminology point of view I'd distinguish between the two languages in means of describing them as "pure" or not.

I also really worry that external proofs will ultimately be neglected in practice. I suppose this is again a "UX of Types" thing, but I'm something of a believer that anything that you do not literally demand of the programmer will eventually be sacrificed.

I'm not totally sure what you mean by "external proofs will ultimately be neglected".