l-calculus is the fundamental underpinning of functional programming Now, the l-calculus is in fact the archetype of such functional programming languages; that we have distinguished in two classes: those called by value, where, whenever you apply a function to an argument you first evaluate the argument, and then you replace it, and those which are called lazy, where you actually replace not the evaluated argument, but the code.
The reason why the function of paradigm is convenient for developing certified software is because functional programs are very close to implicit or recursive specifications. And so you do not really have a very opaque encoding, and moreover you can encode objects and parallelism in a very natural way in functional programming.