Formally verifying the correctness of an algorithm
algorithm, correctness, formal-verification, math, proof
Solution
COQ is a proof assistant that produces correct ocaml output. It's pretty complicated though. I never got around to looking at it, but my coworker started and then stopped using it after two months. It was mostly because he wanted to get things done quicker, but if you need to verify an algorithm this might be a good idea.
Here is a course that uses COQ and talks about proving algorithms. And here is a tutorial about writing academic papers in COQ.
Problem
First of all, is this only possible on algorithms which have no side effects? Secondly, where could I learn about this process, any good books, articles, etc?