7.4.6 C: Units
Type checkers help us make sure we don’t mix up values of different types. However, by definition, they don’t catch mistakes within types. Some common forms of annotation and checking are used in other domains, like units and dimensions.
In science, engineering, and other fields, it is standard to perform such analysis, and failing to do so can lead to catastrophic outcomes. See, for instance, the story of the Mars Climate Orbiter, which had a tragic end, and the Gimli Glider, which was fortunate not to.
One of the most widely-used programming languages, employed by millions of professional programmers and non-professionals as well, is the spreadsheet. In conventional spreadsheets, most data are numbers, making it easy to create meaningless answers. See, for instance, this paper, which discusses this problem, and points to other literature on spreadsheet errors.
After you’ve read these materials (you don’t have to read the paper in full, just skim it; you’ll see the ideas of constraint generation and solution pretty soon in the course), explore Google Sheets to see what support it provides for catching unit errors.