I don't think that is a great example since it only takes a moment to see the loose bounds C, X = 3, e. It would be annoying to have to code that kind of state

I don't think that is a great example since it only takes a moment to see the loose bounds C, X = 3, e. It would be annoying to have to code that kind of statement every time, but it wouldn't add that much to the effort. Formalizing is still enormously hard, but I don't think that this is the example to hang the argument on.