Typically when writing a program, your job doesn’t end with merely writing the code, but you would also want to know some properties your code exhibits. You can arrive at these properties by two means: either by logical analysis or by empirical observation.
Examples of such properties include:
- correctness (does the program do what it is supposed to)
- performance (how long does it take)
- scalability (how is performance affected with input)
- security (can the algorithm be maliciously misused)
When you measure these properties empirically, you get results with limited precision. Therefore mathematically proving these properties is far superior, however it is not always easy to do. Functional languages typically have as one of their design goals making mathematical proofs of their properties more tractable. This is what is typically meant by reasoning about programs.
In terms of functions or lesser units, the above applies, but also sometimes the author simply means thinking about the algorithm or designing the algorithm. It depends on the particular usage.
As an aside, some examples of how one might reason about some of these things and how empirical observation can be made:
Correctness: We can prove that code is correct, if we can show equationally that it does what it is supposed to do. So for a sort function if we can show that any list we give it will have the property of being sorted, we know our code is correct. Empirically we can create a unit test suite where we give our code examples of input and check that the code has the desired output.
Performance & Scalability: We can analyze our code and prove performance bounds of the algorithm so that we know how does the time it takes depend on the size of the input. Empirically we can benchmark our code and see how quickly it actually runs on a particular machine. We can perform load testing and seeing how much actual input can our machine/algorithm take before it folds/becomes impractical.