Do you have any practical advice? Should I learn formal proofs?
Then you can use formal methods. For example in Coq you may do something like:
(* Some algorithm which takes one number as an input, of course you can have it take any arguments *)
Definition the_algorithm (x : nat) : nat :=
...
.
(* Another algorothm which checks that the output is expected *)
(* You can use 'Inductive' or 'Defintion' to define this, each has its benefits and drawbacks *)
(* 'Inductive' is a GADT where instances have valid inputs / outputs *)
(* You can also write the_algorithm as a 'Definition' with some fuel parameter and return an 'option nat' if your function can't be proven terminating, etc. *)
Inductive check_the_algorithm : nat -> nat -> Prop :=
| BaseCase : check_the_algorithm 0 0
| AnotherCase : forall i o, check_the_algorithm i o -> check_the_algorithm i (i * 2)
| ...
.
(* This is the key part, which proves the algorithm is "correct" *)
Theorem the_algorithm_is_correct : forall n, check_the_algorithm n (the_algorithm n).
Proof.
... (* Here you will prove it using tactics *)
Qed.