If you demand that the program terminates (through higher order structural recursion, i. e. by induction) then this would be a proof in type theory. It's called

If you demand that the program terminates (through higher order structural recursion, i. e. by induction) then this would be a proof in type theory. It's called proof by reflection. When Martin Löf (the father of type theory) saw this trick for the first time he apparently exclaimed "but this is not a proof!" so make of that what you will.