Implicative Formulae in the ``Proofs as Computations'' Analogy