In a program code that calculates physical quantities while omitting their units, I found the following calculation:

```
length   = ...                         # in mm (!)
velocity = ...                         # in m/s
time     = (length / velocity) / 1000  # in s

```

Because `length` was not in standard units, I wondered if the `/ 1000` was the correct way to convert the result to seconds.

### Autor's thought process for writing the calculation

To get `time` in standard units, do not use `length` but use `(length/1000)` instead. As the latter is in standard units, everything should work out. Afterwards, I can simplify the expression:

```
  (length/1000) / velocity
= length / (velocity * 1000)
= (length / velocity) / 1000

```

This is akin to a *constructive* proof.

### My thought process for determining the result's unit

As a reader I had a different approach. On a piece of paper, I inserted $1 \mathit{Unit}$ for each variable and computed the result to see if it was in $m/s$. Obviously, I had to do something with the `1000` too, so I replaced `1000` by $m/\mathit{mm}$ because $\frac{m}{\mathit{mm}}=\frac{1000\mathit{mm}}{1\mathit{mm}} = \frac{1000}{1} = 1000$. This resulted in

$$
 \frac{\;\frac{\tt{length}}{\tt{velocity}}\;}{m/mm}
= \frac{\;\frac{mm}{m/s}\;}{\frac{m}{mm}}
= \frac{\;\frac{s \cdot \mathit{mm}^2}{m}\;}{m}
= \frac{s \cdot \left(\frac{m}{1000}\right)^2}{m^2}
= \frac{\frac{s \cdot m^2}{1000^2}}{m^2}
= \frac{s}{1000^2}
= \frac{s}{1\,000\,000}
= 1\, ns
$$

Where did I go wrong, and how do I correctly type check calculations like these?