Formally verifying the correctness of an algorithm

Question

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?

Answer 1

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.

Answer 2

1. It's generally a lot easier to verify/prove correctness when no side effects are involved, but it's not an absolute requirement.
2. You might want to look at some of the documentation for a formal specification language like Z. A formal specification isn't a proof itself, but is often the basis for one.