> 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 p

> 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.