Say I have a program that needs to not divide by zero:
f(x):
if nonzero(x):
return sin(x)/x
else:
return 1
If we divide by zero, we get an error. We can prove that the above function does not error by noting that the first if branch is not taken when x==0, so the possible error from the division can't happen, and we always get a sensible result.
So the question is what does this proof look like in type theory?
I know it must involve dependent types and such, and I've read a few relevant Wikipedia pages, but I don't know how to type nonzero() or division or how to show in type theory that the error can't happen.
(This isn't supposed to have anything to do with zero in particular, I'm wondering in general how type theory handles proving things around such predicates and dependently-typed functions)
