4 ms·

> Tomorrow they can release some static checking tools. Java's JML and C#'s Spec# are similar. If, in order to check a program, you need to supply additional a

> Tomorrow they can release some static checking tools. Java's JML and C#'s Spec# are similar. 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. So let's not conflate these two languages: (0) The whole of Java, and, (1) The collection of Java programs, equipped with JML annotations, that can be statically verified by some given tool. If the annotations express facts inexpressible in Java's type system, and tool performs a sound analysis, then you can prove more safety theorems about the second language. (And if the analysis is unsound, why bother with it?) That both languages happen to have mostly the same surface syntax and dynamics is best regarded as a happy accident. > First, I didn't say unreasonable, but I think it is still more effort. How so? 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. > Second, without dependent types (which require proof, either manual -- which is a lot of effort -- or automatic -- which is rather limited), you can't nearly express the same propositions. I never said otherwise. I only said “using GADTs and DataKinds to express problem domain constraints is a de facto standard practice”. > The advantages and disadvantages of types do not stem from them expressing static propositions -- there are many ways of doing that Merely expressing static propositions is boring. What really matters is proving them. > but from them expressing propositions in a certain way 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. > that influences how the program is organized and how propositions propagate throughout the program. In a modular way: when checking a module Foo, you won't observe a failure of an invariant internal to another module Bar. > Whether propositions about code are best expressed as types or as data-level propositions is an interesting debate, but a rather subtle one; it is certainly not binary. I can see legitimate use cases for expressing propositions as types (most of the time), as well as legitimate use cases for not bothering to represent propositions in a mechanically verifiable manner (when the proof is obvious, only needed in a very small part of the code, and explicit annotations would only add noise). 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. > IMO, it is likely that some propositions are best expressed as types while others are best expressed differently. Whatever makes the proof go through the easiest.

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

pron 10y ago

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