-title: Gears: Low level Formal Representation of code and data

--abstract:

--Reliable computation and predictablity

Various softwares are used in real world. Each of them have to work in a reliable way. A peice of devie contains
millons of lines of code. These programs are written in C, Haskell and so on. The unit of computation of
conventional programming language is of course a function call.
To assure its reliability, the computation of a function should be predictable, but unfortunately
a function may call another functions and it comes back to the original function. 
Proof theory such as Hoare Logic or model checking method is used to make the prediction, such as
zero divide is never occured in a function.

We propose new unit of computation, data segments and code segments. Computations in these segments are finite and
predictable. We sometimes call these gears. A set of gears make programming system. This unit is larger then
an machine instruction and smaller than a function call. Data segments and code segments are connected by
meta data segments and meta code segments. The idea is construct system as a set of predictable unit of
computation.

--Definition of data segment and code segment

We implment our Gears language in LLVM\cite{LLVM},