The paper presents a formal and practical approach to dependable algorithm development. First, starting from a formal specification based on the Eindhoven quantifier notation, a problem is regu-larly reduced to subproblems with less complexity by using a concise set of calculation rules, the result of which establishes a recurrence-based algorithm. Second, a loop invariant is derived from the problem specification and recurrence, which certifies the transformation from the recurrence-based algorithm to one or more iterative programs. We demonstrate that our approach covers a number of classical al-gorithm design tactics, develops algorithmic pro-grams together with their proof of correctness, and thus contributes fundamentally to the dependability of computer software.