I have two binary to decimal conversion methods and want a proof - or an intuition at least - of why they are equivalent.
The first method is quite intuitive to me and seems to be more popular: $[b_n ... b_1 b_0] -> (b_n * 2^n) + ... + (b_1 * 2^1) + (b_0 * 2^0)$
The second method isn't as intuitive, and it would help if someone can explain to me why this works to do just what the previous method does:
$[b_n ... b_1 b_0] -> to\_nat\ [b_0 b_1 ... b_n]$
where
$$
\begin{align}
to\_nat\ b = match\ b\ with \\
&|\ [\ ] \to 0 \\
&|\ [head,\ [tail]] \to if\ (head = 1)\ then\ 1 + 2 * (to\_nat\ tail)\
else\ 2 * (to\_nat\ tail)
\end{align}
$$
Sorry if this notation is confusing. I'm using notation derived from functional programming.
The first method is simply the definition of base-2 representation illustrated in (1) below which is analogous to the definition of base-10 representation illustrated in (2) below and the generalized base-b representation illustrated in (3) below.
(1) $\quad a_n...a_1 a_0\,\text{(base $2$)}=2^n a_n+...+2^1 a_1+2^0 a_0$
(2) $\quad a_n...a_1 a_0\,\text{(base $10$)}=10^n a_n+...+10^1 a_1+10^0 a_0$
(3) $\quad a_n...a_1 a_0\,\text{(base $b$)}=b^n a_n+...+b^1 a_1+b^0 a_0$
Base-10 representation is the primary representation most people have been taught and used, but electrical engineers and software programmers commonly use other representations such as base-2 (binary), base-8 (octal), and base-16 (hexadecimal) representations.
If you calculate the first method by hand you're likely calculating the result in base-10 representation therefore the result will be in base-10 representation.
The vast majority of computers are digital and perform all calculations in binary-representation, but computers typically have input/output libraries with options for entering and displaying results in various bases.
The second method is equivalent to the first method which can be seen from the following example.
(4) $\quad a_3...a_1a_0\,\text{(base $2$)}=2\,(2\,(2\,a_3+a_2)+a_1)+a_0=2^3\,a_3+2^2\,a_2+2^1\,a_1+2^0a_0$