On: Untyped Programs Don’t Exist

[kazinator]

(Only problem is that such a type system is unwieldy compared to mathematics itself.)

[0db532a0 → kazinator]

I suppose we’d better get you in contact with with all those silly mathematicians who like to use proof assistants to add rigour to their work.

[kazinator → 0db532a0]

In run of the mill mathematics, I've never seen zero treated as a special type. In derivations, a restriction against zero (because some variable appeared in a denominator) is usually carried as a logical assertion that is attached to subsequent derivations, like "<.. equation ...>, x /= 0".