> However, you can consider the formal specification of your intent (the type), to be an example of fully declarative programming.
The vast majority of formal specification and verification tools (I believe Coq and Agda are the only exceptions, and they are rarely used in the industry) express the intent directly in logic rather than in the types (HOL in Isabelle and HOL Light, ZFC+LTL in TLA+ and maybe Scade, ZFC in Alloy, and a typed set theory in SPARK, I believe).
> But in practice it's usually enough to catch the sorts of mistakes that you're likely to make.
I think this claim is supported by little evidence. Most non-dependent type systems are extremely weak (or require cumbersome encoding) to express even all but the most trivial of properties (e.g. they can't even express that the value returned from a max function is indeed maximal, let alone more elaborate properties). Their expressive strength is that of a finite-state machine. How much does that prevent real bugs requires empirical study.
The vast majority of formal specification and verification tools (I believe Coq and Agda are the only exceptions, and they are rarely used in the industry) express the intent directly in logic rather than in the types (HOL in Isabelle and HOL Light, ZFC+LTL in TLA+ and maybe Scade, ZFC in Alloy, and a typed set theory in SPARK, I believe).
> But in practice it's usually enough to catch the sorts of mistakes that you're likely to make.
I think this claim is supported by little evidence. Most non-dependent type systems are extremely weak (or require cumbersome encoding) to express even all but the most trivial of properties (e.g. they can't even express that the value returned from a max function is indeed maximal, let alone more elaborate properties). Their expressive strength is that of a finite-state machine. How much does that prevent real bugs requires empirical study.