`fac1 ( n )`

`if n = 0 return 1`

`else return n * fac1(n-1)`
`fac2 (n, m ) // m = n !`

`if n = 0 return m`

`else return fac2( n-1, n * m )`

Which are the two programs illustrated in the correctness proof above.
The two programs are both correct, they both compute factorial of input.
fac2 is called by fac2( n, 1 ). The second program, fac2, is more efficient
because the recursive call is the last call and can be optimised (call
"tail-recursion optimization") which change recursive call into iterative
loop. The style of fac2 is called accumulating parameter.