Modelling strict floating point behavior in math-like dialects

again, I’m not familiar with the details here, but are these even correct w.r.t. the IEEE754 standards in the first place?

I don’t think the C standard has anything to say about this. What are you steering towards?