I think I'm saying that a "formally proven sound" construction that is full of poorly understood traps for the implementer on actual machines is not always the best choice in practice.
Yep. I think we can go farther than that and say that it's been historically screwed up by protocol designers and/or implementers more often than not (with predictable IVs, timing and length oracles, MAC-then-encrypt, etc)
