I actually think dependently-typed languages like Idris are the most promising in this area right now, at least until proof assistants get a lot better. It's a

I actually think dependently-typed languages like Idris are the most promising in this area right now, at least until proof assistants get a lot better. It's also not specifically the rigor in mathematics, but the grounding in solid principles. They have axioms, they know how to prove things, and they know which proofs to trust and why for the most part. What frustrates me most is stuff like programmers haphazardly reimplementing monads over and over again instead of moving on with what they were actually working on before the language and type system got in their way.