Comment by pron | Hacker News Reader

Comment by pron | Hacker News Reader

Parent Full thread

Not all untyped languages are the same. E.g. Clojure now encourages specifying assumptions with spec annotations, some of them are stronger than those that can be expressed by Haskell's type system: i.e. they can succinctly express more about the "entire code" than Haskell's types. Types are not the only way to write formal assertions and assumptions about code. The difference between the two is in the level of sound inference that can be made (stronger with types) and the strength and expressivity of the assertions (stronger with contracts).

Of course, one could say we should have both, and some languages -- like Java with JML, C with ACSL, and SPARK, as well as some research languages like Whiley and Dafny -- do. But this could add complexity, and the interesting question is, if you could just have one, what are the relative merits of either? My guess is that types would be better for enforcing code organization and for tooling (more efficient AOT code generation, safe automatic refactoring, code completion), because automatic transformations require automatic and sound inference, while contracts are better for correctness because they can more easily express stronger properties of interest, and require less effort to verify them (types require formal deductive proofs, while contracts can use those or a range of other techniques that vary in their cost and their soundness).

In short, types are not the only form of formal specification, but the different forms do have different practical characteristics. What matters is not just what we want to know about the rest of the code, but how we want to use that information and how certain we need to be. Unfortunately, theoretical results tell us that we cannot have a perfect system that is always correct, cheap to use, and can allow us to express rich properties.

Techniques like Ghost of Departed Proofs are the most exciting thing to me as a casual correctness enthusiast. It acts as a means of combining static types with contracts.

Types are sound mostly because they are a stupid mini language, so easily enforced, like you said. Contracts are practical and convenient because you tend to write them in the language or a subset thereof that you’re checking. That’s hard to ignore.

GODP has you write a runtime check in regular code, and return as a result a proof value. Put that code in a module boundary. Then you have upstream functions expect a proof argument along with the value the proof is about. They’re tied together with a unique type variable (rank n or existential are the mechanisms of delivery for Haskell, but may differ in other languages).

head :: NonEmpty n -> Named n (List a) -> a

In this way you started from a dynamic, runtime piece of code, and ended up using a static type system to just ensure everything is passed around correctly which is trivial.

A single proof in this technique is nominal in the type (e.g. not null or positive or sorted ascending/descending), but combining them is done at the value level so there’s flexibility.

The bang for buck potential is large. I’m more interested in stuff like this than the dependent types direction that people are pushing for in GHC. If I wanted dependent types I have Agda, Coq, Isabelle, Idris, etc. to play with.

Actually techniques like the Ghost of Departed Proofs are precisely the reason I'm excited about dependent types (although with the caveat that you need some way of talking about erasure).

Contract systems in general have the problem that it is difficult to express higher-order properties about how functions should interact with each other or repeated invocations of themselves. For example, it's rather convoluted to express associativity with a contract system. Contract systems are very well-suited for imperative contexts (see e.g. Hoare Logic), where you have procedures rather than functions and you usually don't think about e.g. whether a procedure is associative or not. They work for functions, but are not as great a fit.

Dependent types allow for further expressivity, and, crucially, as long as you separate theorems from code (that is as long as you don't take Curry-Howard too seriously), there's no reason you're forced to prove a theorem with the type system if you find it too difficult.

Imagine:

concat : List a -> List a -> List a

concat = ...

concatSumsLength : (xs : List a) -> (ys : List a) -> size (concat xs ys) = size xs + size ys

concatSumsLength = proofByPropertyTest concatPropertyTest

concatPropertyTest = (1000 different lists concatenated together and then checking that their sizes add up)

There's no reason that concatSumsLength needs to be satisfied by a true implementation, unless you require that its value be usable at runtime. However, as Idris 2 shows, there's no need for that to be true (or even Coq with Prop vs Type). You can just annotate it as erased at runtime.

If you have a way of ensuring that certain values are never used at runtime, then there is no reason that your proof obligations must be met through satisfying the type checker.

That's an interesting angle. Another way of saying it might be that GoDP on the face of it can make one-off proofs for a value. Proofs for a function requires making proofs about all possible inputs, which is where your property test comes in handy. I could have `Named a (List x -> List x -> List x)` as the function I'm proving things about.

With some template-haskell you could run the property test at compile-time, and then use that proof later (e.g. for an instance of Semigroup which would require a argument proof of associativity), in languages like Unison that never run the same test suite twice (due to Content addressable code), this would be feasible. Or just run the property in your test suite and hope that the developer runs the test suite often. GHC erases data types that aren't actually evaluated in many contexts, so we even have erasure too.

I like your angle!

> Contract systems in general have the problem that it is difficult to express higher-order properties about how functions should interact with each other or repeated invocations of themselves

Contract systems can express anything that can be expressed about a program. Some allow you to specify separate lemmas (e.g. see http://www.eecs.ucf.edu/~leavens/JML/jmlrefman/jmlrefman_toc...) . The difference between dependent types and contract systems is that contract systems can be verified by deductive proofs, or by a host of unsound techniques, while dependent types require deductive proof (or, in some experiments, other sound techniques like model-checking). If dependent types would accept unsound proofs, the soundness of the entire type system would be compromised to the point of undefined behavior.

The problem is that deductive proofs have so far shown significantly worse scalability than other formal methods, which is why most of formal methods research is looking elsewhere.

If dependent types could be made more flexible, they will be as good as contract systems.

> If dependent types would accept unsound proofs, the soundness of the entire type system would be compromised to the point of undefined behavior.

This seems like too strong of a statement. Every language that allows for nontotal functions has a type system allowing for unsound proofs. This does not mean the type system is compromised to the point of undefined behavior.

Dependent Haskell is explicitly going to be unsound even in the presence of totality (type in type). Idris allows for partial functions by default (although you do need to annotate if you want to use it at the type level and the compiler doesn't know it's total). Dependent type systems are not required to be sound by any means.

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

Leaving that aside, my point is that as long as you don't need your proofs at runtime, you don't have to use a deductive proof with dependent types! Substitute the property check thing there with a model checker if you want 100% assurance, but you don't even need a sound verification! If you're okay with just 99% confidence instead of 100% then just do the property test and be done with it (that's my example with concat and chrisdone is talking about when you would run the property test). If you're feeling really adventurous just assert the statement without proof and move on. If you don't run it at runtime how you prove something or even if you do is up to you.

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 suspect you can, but I also suspect it looks annoying and hacky where you essentially encode a function application counter in your ambient state and have to basically make an inductive statement. EDIT: ah ha in JML you have the keyword pure that extends Hoare Logic so I suppose you do an assert with pure? But then how do you express the general notion of associativity? By requiring purity as a precondition and then writing out the condition again? Can you specify purity as a precondition? I'm not sure how you do that, presumably you'd need JML to be able to recognize a SAM class and then be able to tie purity to that, which seems hard if not built-in.

Whereas with dependent types it looks very similar to the usual notation.

  (x, y, z : A) -> x `op` (y `op` z) = (x `op` y) `op` z

For

  op : A -> A -> A

More generally you can express associativity itself with:

  isAssociative : (op : a -> a -> a) -> ((x, y, z: a) -> x `op` (y `op` z) = (x `op` y) `op` z)

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

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.

My guess is that types would be better for enforcing code organization and for tooling ... while contracts are better for correctness

I see what you're getting at, but there is one other crucial difference: the types we're talking about here are usually checked at compile time, whereas the contracts we're talking about here are usually checked at run time. Although the latter may be more expressive if other things are equal, other things are very much not equal in this respect.

How much that matters depends on the nature of the software and how it is to be deployed and used. If you're writing a program for your own use, it might not matter much at all. If you're writing a program that is going to control a satellite and software maintenance after launch is extremely expensive if not impossible, it might matter a great deal.

> whereas the contracts we're talking about here are usually checked at run time

No, they can be checked in many different ways, hence their power. They can be checked "statically", i.e. at compile-time, or dynamically. One approach is sound but requires more effort, while the other is cheap yet unsound -- and there is a spectrum in between the two extremes.

> If you're writing a program that is going to control a satellite and software maintenance after launch is extremely expensive if not impossible, it might matter a great deal.

Such programs often use formal methods that precisely use such contracts. Rich type systems (like Idris's) are virtually never used in practice in those cases. If you've heard of SPARK, it's a language that provides static verification of properties specified as contracts, not as part of the type system, and it is used in some safety-critical realtime applications.

No, they can be checked in many different ways, hence their power.

Sure, but the more dynamic ones that drift away from what a (good) static type system offers are exactly the ones that aren't amenable to automated proofs and so tend to be checked at run time.

Such programs often use formal methods that precisely use such contracts. Rich type systems (like Idris's) are virtually never used in practice in those cases.

As someone who has worked on relatively high-reliability systems, I can say with 100% confidence: it depends. This too is an area with a whole spectrum of possibilities, and some of those involve a degree of formal proof of algorithm properties but not a mechanically verified translation of those algorithms into implementation code. In such cases, a powerful static type system certainly can be a useful safeguard against introducing defects during the translation.

> Sure, but the more dynamic ones that drift away from what a (good) static type system offers are exactly the ones that aren't amenable to automated proofs and so tend to be checked at run time.

Not really. What contract systems allow you to do is to separate specification from verification. Type systems require that all of your specifications be verified with deductive proofs. This means that some deep properties either require a lot of work (using a type system such as Idris's) or are excluded from the type system at all. Contracts allow you to check a property in unsound ways, too.

As far as correctness is concerned, contracts do everything a type system can, but more flexibly. Type systems, however, have advantages related to tooling and efficient code generation by an AOT compiler.

> This too is an area with a whole spectrum of possibilities, and some of those involve a degree of formal proof of algorithm properties but not a mechanically verified translation of those algorithms into implementation code.

Even when formal proofs are used, the specification is done in a contract system, not a dependent type system.

What contract systems allow you to do is to separate specification from verification. Type systems require that all of your specifications be verified with deductive proofs.

I think you're making the same point that I am, but perhaps from the opposite direction.

Of course contracts are more general, but the aspects of a contract that you can prove automatically in advance are similar to what you can typically do with a good static type system, and the limits of a decent static type system fall around the point that contracts become more powerful but only at runtime. This isn't an accident, it's a fundamental equivalence.

For example, you mentioned SPARK before. One of the interesting things about SPARK is the extra flexibility you have when adding constraints on integer data types. The proof system can verify certain properties (or warn you that it can't). That can provide safeguards against, among other things, some very common logic errors like out-of-bounds access to data structures.

However, the fact that we're dealing with integer values is very helpful in this respect. Lots of behaviour is fully specified no matter how much we manipulate those values. For the same reason, dependent type systems can often provide similar guarantees. The curious property of C++ templates that they allow integer as well as type parameters has allowed for all kinds of handy metaprogramming tricks along similar lines.

Now, suppose we're working in the much less convenient world of floating point values. It's still helpful to have warnings about, for example, potential underflow or overflow conditions, for all the same reasons. However, given the inherent imprecision of floating point data, it is impossible to prove such conditions in advance in almost any non-trivial case. You can certainly have a precondition on a relevant function that, for example, adding two input values must not entirely lose the smaller value due to loss of significance, but you won't find out about inputs that violate the contract until you run your program.

Even when formal proofs are used, the specification is done in a contract system, not a dependent type system.

You can do the specification in any number of ways. Unless you want to classify all of mathematics as "a contract system", which is true in a sense but so general as to lose any useful meaning of the term, your statement above is too strong.

Also, the following part isn't necessarily because of dynamic typing vs static

> what types all the variables are, what expectations are attached to them, what mutation, if any, each method call performs

But more about what the language offers. Clojure for example, goes beyond types with it's abstractions (like seq, that can be applied to strings, lists, maps and so on) and normally stays away from mutation, but when needed, makes it really explicit and easy to find those mutations.

Java's JML contract system [1] allows you to explicitly state which mutations a method performs as part of its contract.

[1]: https://www.openjml.org/

> Clojure for example, goes beyond types with it's abstractions (like seq, that can be applied to strings, lists, maps and so on)

Goes beyond types? Statically-typed languages can have polymorphism.

Spec is at heart a data modelling system. So for example,

  (s/def ::integer integer?)

is very explicitly not a definition of an "integer" type. It is preparation to model some data x and check that the data will evaluate to true if someone uses the predicate (integer? x). However, this is obviously enough to implement a type system.

But you can also do some very loose things with spec that aren't done in a type system (I speak with a cheerful ignorance of type systems). Eg, I can spec a function so that one argument is smaller than the second. This allows my testing system to automatically generate the correct data to test my function.

So spec can used to implement a type system but also to implement things that aren't type systems.

> But you can also do some very loose things with spec that aren't done in a type system (I speak with a cheerful ignorance of type systems). Eg, I can spec a function so that one argument is smaller than the second. This allows my testing system to automatically generate the correct data to test my function.

Check out dependent type systems. These allow you to define, mindbreakingly enough, types that __depend on the values you assign at runtime__, and functions whose type depends on the values passed as arguments.

Don't ask me how it's done; it's all dark magic to me. All I know is that people who use dependent type systems claim they are very good at certain uses involving incoming streams of unknown data, like parsing binary protocols.

https://en.wikipedia.org/wiki/Dependent_type

Why is seq “beyond types”? Isn’t it like a Rust Iterator trait?

What do you mean with going beyond types? Is it possible to define some unique compile time constraints on Clojure not related to the type system?

When spec was proposed I remember some talk of compile-time checking of some annotations. I don't know whether anything came of that, but in theory it would allow what you're talking about. That has no relation to seq, though, which is the kind of thing supported by many statically typed languages.

Commented elsewhere here but static languages can do this also via ad hoc polymorphism or bounded polymorphism.

Reply on news.ycombinator.com