I'm currently looking at annotations / decorations to a research programming language to estimate runtime non-asymptotically (i.e. gimme a number) in a simple execution model. I thought there might be (have been) some similar projects, but I'm not really sure where to look. I vaguely remember some work on proving loop bounds (e.g. polyhedrally). Any hints?