Comment by x13pixels

If you are interested in building programs with proofs of correctness, one of the authors of A Tensor Language (ATL), Adam Chlipala, has a book called "Certified Programming with Dependent Types" that can be read at http://adam.chlipala.net/cpdt/