Lambda the Ultimate

A language with those denotational semantics would, it seems to me, would have a difficult time with operational semantics.

Without peeking into function definitions, you can't be sure that an infinite sum converges, there's always the possibility that the next term will be too "large." After evaluating any length-n prefix of the infinite sequence, no matter how fast you have seen it shrinking so far, you can't be sure that the function doesn't evaluate to 37 for all terms after the nth. When does the implementation guess that n is large enough that the sequence doesn't converge and report an error? Alternately, when does it guess that the sequence does converge and report an (approximate) value possibly in error? Such an erroneous report is different from writing an infinite loop, it is still "the programmer's fault", but instead of introducing non-termination it introduces potentially unbounded error.

Discharging the assumption that the sum converges runs into Rice's theorem, and now you are building a more complicated type system to conservatively and statically approximate convergence.

I may be wildly misreading, sometimes the jargon gets me; if so I would appreciate a nudge back on track.

You're not misreading. There are definitely operational issues to work out.

Operationally, it's tricky, as you say. I don't envision a "push Enter and wait for a definite answer" sort of interaction, so there would be no need for any static or dynamic system to determine when a finite approximation is "close enough". I've thought of two alternatives. One is background computation, in which the approximations get better as you wait. It'd be kind of like FRP. The other alternative has the user asking for better and better approximations as he decides he wants them.

In both alternatives, the metric that defines the output value's metric space would be available somehow, so the user could get a "feel" for whether it's converging. If he wants to prove convergence - e.g. for all inputs, the sequence of output values is Cauchy - that'd be analogous to proving termination on all inputs.

The thing that worries me is that it seems the semantics would (roughly) move all the limits to the outside of the program and combine them into a single limit. I'd have to pin down exactly when that's legal, and that seems tricky - and also a lot like domain theory.

I'm not sure I understand what you mean by convergence. Especially in lazy languages, one can have values that are not completely defined, but are not _|_.

For example (1, _|_), or [1, 2, 3]:_|_, where the _|_ is of the appropriate type.

I also recall a paper by Martín Escardó, that starts operationally, defines when a computation is observationally lesser than another computation (whenever the former returns a ground value, so is the latter), and then obtains domains, topologies, convergence, etc. So these notions appear to be in-grained in recursive functions.

I'll try to find the actual paper later today.