§ My disenchantment with abstract interpretation

When I first ran across the theory of abstract interpretation, it seemed magical: Define two functions, check that they're monotone maps, and boom, we have on our hands an analysis.
However, the problem appears to be that in reality, it's not as simple. Here is the list of issues I've run across when trying to use abstract interpretation for a "real world" use-case:
First of all, all interesting lattices are infinte height, requiring some choice of widening. Defining a good widening is a black art. Secondly, while there is a lot of theory on combining abstract domains (reduced products and the like), it seems hard to deploy the theory in the real world.
I read a fair bit into the theory of abstract acceleration, where the idea is that instead of widening indiscriminately, if our theory is powerful enough to compute an exact closed form, we choose to do so. However, the problem is that this regime does not "fit well" into abstract interpretation: We have the abstract interpreter on the one hand, and then the acceleration regime on the other, which is a separate algorithm. So the full analysis looks something like:

def analyze(program):
  analysis = {}
  for loop in inner to outer:
     loop_data = abstract_interpret(loop)
     analaysis.append(accelerate(loop))
  return analysis

That is, what used to be a nice theory of just "do things in any order and it will converge", now becomes a new algorithm, that uses abstract interpretation as a subroutine. This was not the hope I had! I wanted to get away from having to do proofs by analyzing an algorithm, this was the entire promise: Define a lattice well enough and the proof is guaranteed. Rather, what I had imagined was:

def analyze(program):
  return abstract_interpret_using_acceleration_domain(program)

Now this acceleration_domain maybe frightfully complicated, but I'm willing to pay that price, as long as it's an honest-to-god abstract interpretation. This was a huge bummer for me to find out that this is not the case.