[adrianratnapala]

When I was a student in the late '90s, folks at the Uni wanted to that stuff with Ada. I suspect that some limited-but-useful version of this does exist by now in niche sub-branches of safety-critical embedded programming. (Though the commercially used onces are likely to be static analysers for C as they are to be an ADA compiler).

I mean it's nice for compilers to count instructions, but that is far more likely to work on some "primitive" embedded CPU than it is to work on the modern spectre-pipelined goliath CPUs that we use in personal computers and datacentres.