The contributions of this report are twofold. First, we will give the intuition of how programs can be represented in the rewriting calculus. We will compare with the lambda-calculus and take many examples of OCaml programs. Secondly, we propose, study and exemplify a rewriting calculus with explicit constraint handling. In this calculus, matching and application of substitutions become explicit. The approach is really modular, allowing extension to arbitrary matching theories. We will also prove that the calculus is powerful enough to deal with errors. We will afterwards prove the confluence of the calculus and the termination of the ``explicit'' part of the calculus, some non trivial proofs. We conclude by an other extension of the calculus to handle composition of substitutions.