Determine the unit of raw number expressions that also convert between units 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?
 A: Recall that units are just specific quantities, and that the numerical value of a quantity (that is, a pure number which can be stored in a computer's memory) can be obtained by dividing that quantity by a corresponding unit. So, start with the relationship
$$t = \frac{l}{v}$$
and if you want the time in seconds, divide by second
$$t/\mathrm{s} = \frac{l}{v\cdot\mathrm{s}}$$
Then, dividing both the numerator and the denominator by millimeter yields
$$t/\mathrm{s} = \frac{l/\mathrm{mm}}{v\cdot\mathrm{s}/\mathrm{mm}}$$
And, finally, multiplying and dividing at the denominator by the wanted speed unit yields
$$\begin{align}t/\mathrm{s} &= \frac{l/\mathrm{mm}}{v/(\mathrm{m}/\mathrm{s})\cdot (\mathrm{m}/\mathrm{s})\cdot\mathrm{s}/\mathrm{mm}} \\
&= \frac{l/\mathrm{mm}}{v/(\mathrm{m}/\mathrm{s})\cdot \mathrm{m}/\mathrm{mm}} \\ 
&= \frac{l/\mathrm{mm}}{v/(\mathrm{m}/\mathrm{s})\times 1000}\end{align}$$
The last line above corresponds to the last equation in your code. Or you can operate the other way round, starting from the equation in the code:
$$\frac{l/\mathrm{mm}}{v/(\mathrm{m}/\mathrm{s})\times 1000} = \frac{t}{\mathrm{s}\times 1000\,\mathrm{mm}/\mathrm{m}} = t/\mathrm{s}$$
Note that even though the variable name in the code is length, it contains the numerical value $l/\mathrm{mm}$ and the variable velocity contains the numerical value $v/(\mathrm{m}/\mathrm{s})$. The result gives the numerical value $t/\mathrm{s}$, that is, the time measured in seconds.
Quantity calculus is the key to solve all these kind of problems!
A: You replaced only a part of the conversion factor.
The author converted using the factor 1/1000. When type checking, you have to replace that entire conversion factor. $1 / (mm/s)$ would yield the correct result of $1\,s$.
General approach for type checking raw number expression

*

*Spot the constant numbers from which you think that they are used for unit conversion, for example:

*

*powers of ten (10, 100, 1000, ... and 0.1, 0.01, 0.001, ...)

*constants for time, e.g. 365, 24, 60, 3600

*constants for angles, e.g. 360, 180, 90; $\pi$, $\tau$; 400, 200, 100

*and a huge load of other constants in case you have to deal with the imperial system



*Rewrite the expression so that the numbers from step 1 are written as separate factors in front of everything else, e.g.
$$1000\cdot\frac{1}{3600}\cdot\ldots\cdot(\text{ expression without unit conversion })$$

*Replace each of the extracted numbers by equivalent fractions of units. The numerator is the output unit and the denominator is input unit of the conversion, e.g.
$$(\mathrm{km}/\mathrm m)\cdot \frac{1}{(\mathrm h/\mathrm s)}\cdot\ldots\cdot(\text{ expression without unit conversion })$$

*For each variable insert $1\,\mathrm{Unit}$ and calculate the result.

A: If we use [square brackets] as an operator that means "the units of," we have
$$
\left[
\frac{\tt{length}}{\tt{velocity}}
\right]
= 
\frac{\text{mm}}{\text{m/s}}
= \text{s}\frac{\text{mm}}{\text{m}}
$$
We know that $\rm 1000\,mm = 1\,m$, or equivalently that $\frac{1\,\mathrm{m}}{1000\,\mathrm{mm}} = 1$. And we can multiply or divide by one without changing the value of our expression. So we can say
$$
\mathrm s \frac{\mathrm{mm}}{\mathrm m}
=
\mathrm s \frac{\mathrm{mm}}{\mathrm m} \times 1
=
\mathrm s \frac{\mathrm{mm}}{\mathrm m}
\times \frac{1\,\mathrm m}{1000\,\mathrm{mm}}
$$
This is exactly equivalent to, but sloppier than, the approach in Massimo's answer of writing $\frac{v}{\mathrm{m/s}}$ to refer to the numerical value of $v$ in some specific unit.
The notation "$\mathit{variable}/\mathrm{unit}$" is specifically encouraged by the BIPM, which defines the SI unit standard.
However, as a practical matter, I find that the formal approach produces enough denominators-in-denominators that I have to do a handstand about them; handstands are not among my skills. My approach is convenient if you are working on a piece of paper, where you might write something like
\begin{align}
\ell &= 7\,\mathrm{mm}
\\
v &= 10\,\mathrm{m/s}
\\
t = \frac\ell v 
&= \frac{7\,\mathrm{mm}}{10\,\mathrm{m/s}}
\color{lightgray}{\times 1}
\\
&= \frac{7\,\mathrm{mm}}{10\,\mathrm{m/s}}
\color{lightgray}{\times\frac{1\,\mathrm m}{1000\,\mathrm{mm}}} = 7\times10^{-4}\,\mathrm s
\end{align}
In this approach your unit conversion is "done" when all the units you dislike are, algebraically, cancelled out.  So if you are converting a volume you would multiply or divide by
$1^3 = \left(\frac{1\,\mathrm{m}}{1000\,\mathrm{mm}}\right)^3$
