Mathematics and Programming Languages

As you might expect, coming from a math background I prefer more carefully-typed languages. But here I want to describe how mathematical discourse is less formal or general than you might expect, and the lessons that holds for programming.

Note: For brevity, in what follows I assume a very little bit of math background.

Implicit type conversions

It sometimes happens that math uses implicit type conversions. For example, complex numbers are often defined as ordered pairs of real numbers. With this definition a real number is not a complex number. There is of course an obvious isomorphism between the real numbers and the subset of the complex numbers that are of the form $(r,0)$. So no one but a pedant would insist on always writing $(r,0)$ instead of $r$.

However, sometimes strongly-typed programming languages can be pedantic in just this way. This argues for the ability to define implicit type conversions.

Sometimes you need to be specific

Sometimes, you need to be specific in order to be correct, and it may be difficult for a reader to simply infer what you mean without that specificity. For example, in a group theory context, something might only hold for finite groups. But if you aren't specific, it may be easy to guess from context that you intend it to apply to a group, but much harder to be clear that you mean to limit it to only finite groups. Nor may it be easy to see that limitation by inspection. Nor would something analogous to a software 'runtime check' work. (Yes, I'm aware that there isn't a commonly used mathematical analogue of the software notion of checking things at run-time, combined with a thorough testing strategy. I'm skeptical that such an approach to even software development works well, though the matter bears more discussion.)

You needn't always be as general as possible

Oftentimes in mathematical discourse it isn't worth it to be as general as possible. Similarly, in programming, it may not be worth it to be as general as you can.