Hi, I am a Software Engineer (mainly C++, Rust) currently started getting really interested in Formal Program Verification and interesting programming languages (like: Idris, Agda, ATS, HOL, Curry, Mercury and of course Coq etc…) and also proving Real Analysis theorems that I learned a while ago while I was studying at university a few years back but now by using a computer.

I myself really think that mathematical theorems should be organized in a manner like software libraries on computers and this is how I would like use them and work with right now while proving mathematical theorems.

Now, I want to ask: Is it really possible to use Coq alongside learning Real Analysis and Measure Theory and use it for proving important theorems in those fields? Real Analysis I already know quite well but I want to study it again using a book teaching it from the ground up that goes deeper into what I already learned and also I want to learn Measure Theory (I’ve already read about a quarter book on the subject).

Thanks, And if you have interesting links that deal with the subject please share with me.