It depends on your type system. In new languages like Idris or F* you can encode in the type the correctness of an algorithm and it will not compile if the compiler can not prove that correctness.

For example I can prove my my string reverse works in Idris (https://www.stackbuilders.com/news/reverse-reverse-theorem-p...). Or I could prove that my function squares all elements in a list. Etc.

Now a big part of the problem is expressing with sufficient accuracy what the properties of the algorithm you want to prove are. For example for string reverse I may want to show more than that `reverse (reverse s) = s`. Since after all if reverse does nothing that would still be true. I would probably want to express that the first and last chars swap when I just call reverse xs.