Usually because the people capable of writing formally-verified software do not understand the specific subject area, and the people that understand the subject area are not generally capable of writing formally-verified software.
For a perspective of a mathematician that came to evangelize theorem provers, I recommend Kevin Buzzard's MS 2019-09 presentation [0] about LEAN. He highlights cultural misunderstanding and apathy on both sides of the domain divide. He also references the idea that the people who might make the appropriate tools may not have stayed in academia. So, he's structured his courses around using LEAN with the indirect consequence that power users (undergrads) may choose to become open source committers.
[0] https://www.youtube.com/watch?v=Dp-mQ3HxgDE One hour of presentation and then 15 min of q/a. My favorite is around 1:04:00 when someone asks a second time why he disprefers coq, and Buzzard complains that it can't represent some advanced quotient type that he'd have to work around. I'm reminded of [1]
Despite what people may have told you, writing formal software is a quite mathematical task requiring people involved to really engage and write decent software specifications to begin with.
contravariant|6 years ago
Nzen|6 years ago
[0] https://www.youtube.com/watch?v=Dp-mQ3HxgDE One hour of presentation and then 15 min of q/a. My favorite is around 1:04:00 when someone asks a second time why he disprefers coq, and Buzzard complains that it can't represent some advanced quotient type that he'd have to work around. I'm reminded of [1]
[1] https://prog21.dadgum.com/160.html Dangling by a trivial feature
raister|6 years ago