I appreciate the resources and recommendations. I've been interesting in Rocq (formerly Coq) recently, and I've seen dependent types mentioned, so I've been curious to learn more.
On that note, I discovered Dafny[1] recently, as a more accessible way to program with proofs. There's a companion book[2] that seems very accessible and down-to-earth (and, unfortunately, quite expensive). I didn't have the time to play with it yet, but it looks like it does what Ada/SPARK does (and more), but with less verbose syntax and more options for compilation targets. It seems to be actively developed, too. Personally, I had a very hard time getting into Coq, which is a proof assistant more than a programming environment - Dafny seems much more welcoming for a "working programmer" :)
I appreciate even more ideas to work with. A more "working" proof language sounds interesting. While I agree that Rocq is decidably not for a "working programmer," I've had a lot of fun working through the book "Software Foundations". Last night, I was able to formally prove the pumping lemma for regular languages, and that was very satisfying and enjoyable. Another reason I'm learning Rocq is due to my (largely uninformed) interest in homotopy type theory.
