That's where more advanced type systems shine. You get to encode things like "this number is not null" and a safe division function will only take "not nulls" a

That's where more advanced type systems shine. You get to encode things like "this number is not null" and a safe division function will only take "not nulls" as the input. The workflow would then be: 1. prove that the input is not null (if input == 0) yielding a "not null number" 2. running your calculation (no check needed for multiplication or division, if you add something you have to reprove that the number is not null)