Learn Rooster
Coq, proof assistant

The more than five hundred pages of the Coq reference manual should not frighten the future user. Coq is intended to be a very complete program, with numerous tools to help the user develop correct demonstrations. In just a few days, you'll be able to prove the correctness of small, simple functional programs such as the sorting function given as an example in this article. This can be achieved by working through the many tutorials or more comprehensive books