3 ms·

You can't prove intent. However, you can consider the formal specification of your intent (the type), to be an example of fully declarative programming. Since

You can't prove intent. However, you can consider the formal specification of your intent (the type), to be an example of fully declarative programming. Since you write your type without any care about how it might be executed -- the holy grail of abstraction -- you are less likely to make errors. When using a type system that isn't capable of fully specifying what you're doing (i.e. Haskell), you are of course subject to making implementation errors within the range of possible programs that type check. But in practice it's usually enough to catch the sorts of mistakes that you're likely to make.

pron 10y ago
> 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.