2 ms·

> If you lie to the type system you just blow up at runtime, e.g. with an exception. Same as in any other language. That depends on the runtime type system. If

by pron 7y ago

> If you lie to the type system you just blow up at runtime, e.g. with an exception. Same as in any other language. That depends on the runtime type system. If you can switch an int for a string (which is not hard in a dependent type system -- rely on the output of some silly arithmetic function that you only tested and omit a proof and use it in some function that indexes types by integers, and you just might cast an int to a string), you will more likely get some UB and quite likely a security problem. That's why I think that when it comes to correctness contracts are superior to types, and when it comes to tooling and organization, types are superior to contracts. Functional correctness is one area where flexibility is crucial, and soundness is never required because it's impossible anyway. Types, which are used for automatic transformation and code generation is one area where soundness is quite important; we shouldn't mix the two. > Also out of curiosity, how do you express that, say, a static method with two arguments is associative in JML or any other contract system, Hoare Logic based or otherwise? I don't know the arcana of JML, but I see no reason why, at least in principle, you couldn't do the same thing: pure \forall A x,y,z; foo(x, foo(y, z)) == foo(foo(x,y),z) There's also no reason not to define a predicate `isAssociative`. However, there is a difference -- not between specification with dependent types and contract systems, but between the semantics of the language where expressions mean something similar to "partial functions" (or even something similar to functions) and a language where they mean something else (like predicate transformers). In the latter, we don't in general represent computation as functions, so specifying something like associativity would normally be done as follows: define `isAssociative` on functions (not computations), and then specify that a computation computes a function (that is associative). That's how I would do it in TLA+, for example; I think that in Why3 as well. Finally, it's important to remember that the very concepts can be different among languages. For example, all specifications of "higher-order" computations in functional languages (i.e higher order subroutines) become first order when you describe them in TLA+ (https://pron.github.io/posts/tlaplus_part3#higher-order-computation https://pron.github.io/posts/tlaplus_part3#higher-order-comp...). Lamport had this to say: > Comparisons between radically different formalisms tend to cause a great deal of confusion. Proponents of formalism A often claim that formalism B is inadequate because concepts that are fundamental to specifications written with A cannot be expressed with B. Such arguments are misleading. The purpose of a formalism is not to express specifications written in another formalism, but to specify some aspects of some class of computer systems. Specifications of the same system written with two different formalisms are likely to be formally incomparable… Arguments that compare formalisms directly, without considering how those formalisms are used to specify actual systems, are useless. The difference here is, then, not between specifying with types or with contracts, but between different formalisms.

dwohnitmok 7y ago
Well sure if you lie to your specs all bets are off. Buffer overflows, bounds checking, use after free (if you're in a non-GCed language), resource leakage, etc. You're always at the mercy of your runtime system as soon as you lie about your pre-runtime checks, no matter what system you use, types or otherwise. That's different than UB in the type system itself, which if you lie to it at worst just becomes inconsistent, but although that sounds quite scary, it's not really a big deal if you're not using dependent types as a theorem prover and you know where the inconsistency stems from. Now perhaps your contention is that dependently typed systems tend to have weaker runtime checking, which I still disagree with. You do have weaker runtime guarantees with Idris 1's native code generator and of Agda's code extractor, but this is not true of Idris 1 on JS or its other code generators, which inherit their hosts' runtime systems, or Idris 2's native code generator, which inherits Chez Scheme's runtime system. RE computations and functions yeah I definitely overreached. I somehow completely forgot that Hoare Logic has the ability to have unrestricted first-order logic. I got too fixated on JML, where in retrospect the difficulties only come from the awkward way that Java tries to handle higher-order methods like reduce (that was my initial impetus, verification of parallel reduce). I totally forgot I've done the isAssociative property in Dafny before and there it's exactly as you say, it's a function that you then put on top of a method (Dafny's notion of "computations"). The Lamport quote is a good reminder not to poo-poo different formalisms, but I've had a great time with systems like Dafny. I don't think dependent types are the holy grail of verification. My contention in fact is that the gulf between dependent types and contracts is not as large you're making it out to be. Dependent types break down if you have pervasive mutability, i.e. as in an imperative language, for which Hoare Logic is very well-suited for. You have to express the mutability at a type level that's also is transparent enough to the type system to make assertions which makes things very annoying. (And no I don't use mutability/imperative as dirty words, most of my day-to-day work is in imperative languages and that's just fine by me, a lot of algorithms flow more naturally as imperative ones). But if you have a language where everything is immutable, dependent types are fantastically expressive. And as long as you don't use the type inhabitants at runtime, their "proofs" or lack thereof are also very flexible. Hell, you could even generate a runtime assertion from a dependent type if you wanted to and have the compiler automatically insert those in place! You could even do that generation in a user-defined library without compiler support if dependently typed languages supported typecasing and didn't impose parametric polymorphism in all cases (useful in a non-dependently typed language, less useful in a dependently typed one). They don't, but that's a different story (for all my excitement about dependently typed languages, there's so many other ergonomic hurdles to get over first, as is true of a lot of the current state of code-based verification tools). Indeed, dependent types and contracts converge in many ways if you have pervasive immutability. The main difference is that dependent types are more integrated into the language and don't have as many contract-isms. An invariant required by a function becomes just another argument. A lemma is just another function. Those contract-isms are necessary in a mutable environment (it would be rather painful to try to drum up some sort of type-indexed loop monad to try to express the notion of a loop-invariant in a dependently typed language, especially if the loop accesses non-local resources), but are not so much in an immutable one. Oh BTW, speaking of limitations of formalisms, I'm pretty sure you're right on Twitter that Hillel Wayne's hyper-property isn't actually truly a hyper-property and can be described with the temporal quantifiers TLA+ has. A better example (that I don't think can be expressed in TLA+) is something like "variable independence," the statement that for any behavior where a variable "a" takes on some trace, there is another behavior such that "a" has a different trace, but all other parts of the behavior are the same. That is you can delete "a" from your spec and nothing would look different, no behavior would ever change (this requires either quantifying over all predicates or manipulating behaviors directly). Another example would be something like "x 'usually' takes n steps" for some definition of usually (mode, median, average, anything that's not a strict upper bound). Even expressing "n steps" in TLA+ is kind of wonky, but do-able with an additional counter variable (although that makes TLC unable to check termination). Oh and of course since you've linked your own TLA+ link, many many thanks for your TLA+ series. It was an invaluable source right alongside Lamport's own materials when I was learning TLA+ on my own.

by pron 7y ago

dwohnitmok 7y ago

Well sure if you lie to your specs all bets are off. Buffer overflows, bounds checking, use after free (if you're in a non-GCed language), resource leakage, etc. You're always at the mercy of your runtime system as soon as you lie about your pre-runtime checks, no matter what system you use, types or otherwise. That's different than UB in the type system itself, which if you lie to it at worst just becomes inconsistent, but although that sounds quite scary, it's not really a big deal if you're not using dependent types as a theorem prover and you know where the inconsistency stems from. Now perhaps your contention is that dependently typed systems tend to have weaker runtime checking, which I still disagree with. You do have weaker runtime guarantees with Idris 1's native code generator and of Agda's code extractor, but this is not true of Idris 1 on JS or its other code generators, which inherit their hosts' runtime systems, or Idris 2's native code generator, which inherits Chez Scheme's runtime system. RE computations and functions yeah I definitely overreached. I somehow completely forgot that Hoare Logic has the ability to have unrestricted first-order logic. I got too fixated on JML, where in retrospect the difficulties only come from the awkward way that Java tries to handle higher-order methods like reduce (that was my initial impetus, verification of parallel reduce). I totally forgot I've done the isAssociative property in Dafny before and there it's exactly as you say, it's a function that you then put on top of a method (Dafny's notion of "computations"). The Lamport quote is a good reminder not to poo-poo different formalisms, but I've had a great time with systems like Dafny. I don't think dependent types are the holy grail of verification. My contention in fact is that the gulf between dependent types and contracts is not as large you're making it out to be. Dependent types break down if you have pervasive mutability, i.e. as in an imperative language, for which Hoare Logic is very well-suited for. You have to express the mutability at a type level that's also is transparent enough to the type system to make assertions which makes things very annoying. (And no I don't use mutability/imperative as dirty words, most of my day-to-day work is in imperative languages and that's just fine by me, a lot of algorithms flow more naturally as imperative ones). But if you have a language where everything is immutable, dependent types are fantastically expressive. And as long as you don't use the type inhabitants at runtime, their "proofs" or lack thereof are also very flexible. Hell, you could even generate a runtime assertion from a dependent type if you wanted to and have the compiler automatically insert those in place! You could even do that generation in a user-defined library without compiler support if dependently typed languages supported typecasing and didn't impose parametric polymorphism in all cases (useful in a non-dependently typed language, less useful in a dependently typed one). They don't, but that's a different story (for all my excitement about dependently typed languages, there's so many other ergonomic hurdles to get over first, as is true of a lot of the current state of code-based verification tools). Indeed, dependent types and contracts converge in many ways if you have pervasive immutability. The main difference is that dependent types are more integrated into the language and don't have as many contract-isms. An invariant required by a function becomes just another argument. A lemma is just another function. Those contract-isms are necessary in a mutable environment (it would be rather painful to try to drum up some sort of type-indexed loop monad to try to express the notion of a loop-invariant in a dependently typed language, especially if the loop accesses non-local resources), but are not so much in an immutable one. Oh BTW, speaking of limitations of formalisms, I'm pretty sure you're right on Twitter that Hillel Wayne's hyper-property isn't actually truly a hyper-property and can be described with the temporal quantifiers TLA+ has. A better example (that I don't think can be expressed in TLA+) is something like "variable independence," the statement that for any behavior where a variable "a" takes on some trace, there is another behavior such that "a" has a different trace, but all other parts of the behavior are the same. That is you can delete "a" from your spec and nothing would look different, no behavior would ever change (this requires either quantifying over all predicates or manipulating behaviors directly). Another example would be something like "x 'usually' takes n steps" for some definition of usually (mode, median, average, anything that's not a strict upper bound). Even expressing "n steps" in TLA+ is kind of wonky, but do-able with an additional counter variable (although that makes TLC unable to check termination). Oh and of course since you've linked your own TLA+ link, many many thanks for your TLA+ series. It was an invaluable source right alongside Lamport's own materials when I was learning TLA+ on my own.