# Bridging inductive natural number and bits?

Most popular representation for the natural numbers in type systems is:

  Inductive nat : Set :=
| 0 : nat
| S : nat -> nat.


However, digital computers usually represent numbers as bit sequences, arranged into bytes.

The above inductive definition is fine for highly theoretical needs and mathematical proofs, but quite far from and inefficient for real computations, especially, with a very large numbers. Even addition causes a lot of operations.

There surely also are formal verification abstractions for the bit-arrays.

The question is, how to bridge these two representations, for example, to transform a program, using S and 0 into a program, which uses more efficient type for N-byte number (maybe, it's called bit-vector - not sure)?

Of course, limitation to the size of the number may apply.

Are there any theories, which deal with automatic conversion of a program expressed in S-0-notation to a program in "bit-vector" notation and operations? Maybe, there are some stable approaches and even optimizing translators to that?