> If, in order to check a program, you need to supply additional annotations, you aren't checking the original program - you are checking the extended annotated program.
I don't understand what you're saying. The annotations express propositions about the code, i.e. the original program. You could say that typing is also "supplying additional annotations" in a type-level language. I don't understand your definition of "language" in this case.
> All you have to do is think what properties you want to hold for your system. But this is something you have to do whether you encode these properties in types or not.
Not quite because 1/ there are very few properties of programs you can express without dependent types, and 2/ the language used to express the properties is usually very different from the data-level language (except in some languages with dependent types, but those have their own many drawbacks) and often requires clever tricks and thought not about the proposition but about how to express it.
> Merely expressing static propositions is boring. What really matters is proving them.
What matters is verifying them to the possible or desirable degree. Proving most interesting propositions may often be too time-consuming or downright unfeasible.
> In a compositional way: the types of expressions can be synthesized from those of their subexpressions, and the types of defined symbols can be recovered from their definitions' right-hand sides.
This is true for most ways of expressing propositions and is not unique to types. In fact, type inference is more limited than "spec inference", because every expression usually belongs to a single type only (assuming no subtyping). So, e.g., from the expression `x = 3` you can infer only the type judgment `x:Int`, but you can infer many relevant propositions, like `x ∈ Int`, `x ∈ Nat`, `x ∈ {1, 2, 3}`, `x < 50` and `x = 3`. This can be both an upside or a downside for either system.
What is unique to types is indeed some level of modularity (on the one hand, and lack of modularity on the other -- it's complicated). Also, types, because they are a syntactic construct, enforce certain structure on the code which may be beneficial (or not).
> In a modular way: when checking a module Foo, you won't observe a failure of an invariant internal to another module Bar.
This is not so simple. You don't observe a failure provided that the type of Bar fully expresses every property that may affect Foo. I.e., Foo is not allowed to assume anything about Bar other than what is expressed in the type -- that's OK -- but it can't even inquire about it (and let the checker tell you whether the answer to your inquiry is true or false). For that to be truly modular, the author of Bar has to encode every potentially interesting property of Bar, and none of the properties that may change due to Bar's implementation; this is very hard to do right. At the extreme, your type must encode the full denotational semantics of Bar, making none of it internal, on the other hand, this allows the author of Bar to cleanly hide some properties (OTOH, hiding properties is also possibly in untyped specs). This is, again, both an advantage and a disadvantage. Overall, once interesting properties are expressed (through dependent types), I don't think types have a clear modularity advantage anymore.
Another problem with types is that a type is more than a proposition: it is a specific construction of the proposition. OTOH, when you state propositions directly, the expressions `x ∈ Nat ∧ x < 3`, `x ∈ {0, 1, 2}`, `x ∈ Int ∧ 0 ≤ x ≤ 2` all denote the same proposition; in that respect they are more modular than types (I believe, though I may be wrong -- I'm far from a type expert -- that when using dependent types you may need to take into account definitional equality which makes this extensional equivalence tricky).
To summarize, I think that even among type enthusiasts, the question of whether types are always the best way to express (static) propositions about code is an open one. Too little is known about how well either approach works well in practice.
> I can see legitimate use cases for expressing propositions as types (most of the time),
In practice, though, this is rarely the case. Even those few programs that are fully verified deductively usually use a language like Isabelle/HOL, where most interesting propositions are not expressed as types. AFAIK, there has only been a single nontrivial (though still rather small) real-world program ever written that uses types to express all interesting properties (CompCert) and even Xavier Leroy didn't bother proving termination (he says it was too hard/tedious, so he just put a counter, and emits a runtime error if it runs out).
> But I can't see a use case for expressing yet not proving nontrivial propositions that you expect to hold. If it isn't trivial, you need a proof.
What do you mean by "need"? And what do you mean by "proof"? Obviously you don't need formal proof because 99.999% of software written don't prove their interesting, non-trivial properties. Sometimes you want or need a certain level of confidence. That confidence can be provided by a manual or automatic deductive proof, an automatic model-theoretic proof, or something less than proof, like auto-generated tests.
To summarize, I think that even among type enthusiasts, the question of whether types are always the best way to express (static) propositions about code is an open one. Too little is known about how well either approach works in practice.
P.S.
As to observing failure, it's even more complicated than just a matter of which proposition to express in types -- which may be hard in and of itself -- but also some failure modes may be very hard to express using types altogether because they don't naturally lend themselves to denotational semantics (e.g. time and space complexity). Not that those are easy to express in Clojure's spec, and not that they are necessarily a problem with types, only with typed LC, but still (they're easy to express in TLA+).
> I don't understand what you're saying. The annotations express propositions about the code, i.e. the original program.
If you add JML annotations to a Java program, one point of view is that the annotations are external and you're just proving properties about the original unannotated program. I contend that a more useful point of view is that you actually have written a program in another language that happens to be a subset of Java. The safety theorem for the sublanguage rules out more ways of “going wrong” than Java's safety theorem. This is consistent with the fact you wouldn't accept the program if the supposedly “external” SAT solver or type checker or whatever rejected it - you'd check why the tool rejected it.
> You could say that typing is also "supplying additional annotations" in a type-level language.
If you remove the type level from, say, ML, what you get isn't ML anymore. Actually, it isn't even a well-defined language, since ML's dynamic semantics only assigns a meaning to well-typed programs. But, even if you extend ML-minus-types' dynamic semantics to give a meaning to every well-formed syntax tree, its safety theorem will rule out a different set of misbehaviors than ML's.
> I don't understand your definition of "language" in this case.
A programming language is a possibly infinite collection of programs, and is generated from three finite components: a grammar, a static semantics and a dynamic semantics. The static semantics determines which syntax trees are considered valid programs, and the dynamic semantics assigns a meaning to every valid program. I didn't expect to have to provide such an obvious definition here.
> Not quite because 1/ there are very few properties of programs you can express without dependent types.
Plain parametric polymorphism and substructural types can enforce security policies (who gets to manipulate certain kinds of data and how often) and conformance to communication finite-state protocols. GADTs and DataKinds can extend this to protocols with an unbounded number of states, as well as enforce invariants of data structures. (GADTs probably count as a limited form of dependent types, though.)
> and 2/ the language used to express the properties is usually very different from the data-level language (except in some languages with dependent types, but those have their own many drawbacks)
That's a limitation of your tooling.
> and often requires clever tricks and thought not about the proposition but about how to express it.
In what meaningful sense can you claim to have a proposition if you don't know how to express it?
> So, e.g., from the expression `x = 3` you can infer only the type judgment `x:Int`
What you can infer from the definition `x = 3` varies from one language to another. While ML will indeed only infer `x: int`, this is just because ML's static semantics lacks a notion of definitional equality for term-level identifiers.
> Foo is not allowed to assume anything about Bar other than what is expressed in the type -- that's OK -- but it can't even inquire about it (and let the checker tell you whether the answer to your inquiry is true or false). For that to be truly modular, the author of Bar has to encode every potentially interesting property of Bar, and nonproper e of the properties that may change due to Bar's implementation.
Again, depends on your type system. With dependent types, `Bar` can have a rather uninformative type (say, `int`), and separately but in the same context, you can provide a witness `p` of some useful property of `Bar` (say, that it is prime). If the language has a module system, this lets you control how much knowlege you give others about `Bar`. It isn't true that you need to cram absolutely everything you want others to know about `Bar` in its type.