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 "Certifie

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/ http://adam.chlipala.net/cpdt/