Z notation is the framework which left me with this conclusion. It was allegedly named this by its founder because it is "the ultimate" language. I thought it was terrible.
I've used plenty of type systems, and they have all provided a means to annotate the code and then prove certain properties about the code, but I have never in my life seen a type system which let me define a whole specification as formal verification does.
I have also seen type systems go waaaay overboard. They ended up inhibiting development velocity because they were so intent on forcing the programmer prove of the code properties that actually didn't need to be proven.
In general, I think type systems that try to strongly limit the scope of the properties they are trying to prove and apply a cost/benefit trade off to the value of the proven properties and the costs of the annotation work best.
I've used plenty of type systems, and they have all provided a means to annotate the code and then prove certain properties about the code, but I have never in my life seen a type system which let me define a whole specification as formal verification does.
I have also seen type systems go waaaay overboard. They ended up inhibiting development velocity because they were so intent on forcing the programmer prove of the code properties that actually didn't need to be proven.
In general, I think type systems that try to strongly limit the scope of the properties they are trying to prove and apply a cost/benefit trade off to the value of the proven properties and the costs of the annotation work best.