[pron]

> I don't think human programmers have any hope of ever being able to maintain noncompositional program properties for nontrivial programs

We do it all the time. Whatever it is that you want your program to do, and any interesting functional property of it, is a non-compositional property. I know that because if it were compositional, you wouldn't need to write the program. A property P is compositional with respect to terms A and B and composition ∘, if P(A) and P(B) implies P(A∘B) (or more strongly, iff). Compositional and inductive are the same thing if A and B can be any language term. For example, type preservation is a compositional property for, say, ML, and memory safety is a compositional property for, say, Java.

> a human working on the codebase will still need a deductive-proof-like understanding.

I think this is not true, either in principle or in practice: https://pron.github.io/posts/people-dont-write-programs I know I certainly don't have anything close to a deductive understanding of the program I'm working on, but I do have such understanding of the specific pieces of code I'm writing. This is insufficient for a useful formalization of a program, because correctness properties aren't compositional, meaning that, in general, a sound specification of a program component would either be insufficient or unhelpful (i.e. no easier than the code itselg) for the writing of other components. Sure, in some cases it can be, but those are usually the easy cases. We need help with the hard ones.

I totally agree that we try to isolate components and expose them with APIs, but 1. the specification here is imprecise and "soft", and 2. as the results in my "correctness and complexity" show, this does not necessarily make deduction easier (https://news.ycombinator.com/item?id=20714920).

But what you should be asking is this: as there haven't been any major relevant breakthroughs in formal logic in the past couple of decades, nor in any relevant proof techniques (we still use deduction for safety properties), our deductive proof capabilities aren't significantly higher now than they were 30 years ago. If it's all a matter of discipline, then, how come we're still not able to affordably (or at all, if the programs are not tiny) verify programs with deductive proofs?

> how's that any different from what I'd do using any other technique?

I'm not sure I understand the question, but the last thing you want is a rich specification language that forces you to use a particular verification technique, and that's exactly what dependent types do. You want to specify whatever helps you, and then you want to verify using whatever technique you need or can afford, to reach the appropriate level of cost/benefit for your requirements.

> But isn't it much the same process with a detached proof of the program property?

To be honest, I don't know that dependent types are harder than "detached" deductive proofs, but this is something that Neel Krishnaswami (who's an advocate of dependent type advocate) mentioned to me as his observation (he's also the one who told me about attempts to build "gradual" dependent types to alleviate some of the other downsides I mentioned.) This can also be an upside, because it may making writing some proofs easier, as you write the program with them in mind. Either way, I think deductive proofs are, at the moment, too far behind other verification techniques to contrast different kinds of deductive proofs. But this certainly strikes me as an engineering problem.

[Hercuros]

I also mentioned this in my other post, but the CompCert compiler is a highly non-trivial example of a program verified using dependent types, and which would not really be possible using automated methods. Of course, not very affordable, since it took years of work from people with expert knowledge. But you get what you pay for, although the price isn't worth it for most real programs in industry.

Furthermore, you don't necessarily need to have an intuition about why the program you are working on is correct to formalize it using dependent types. You just need an intuition about a method for CHECKING that the program is correct.

The four-color theorem was proved in Coq, and it required considering over a thousand cases. No one can keep a proof of this magnitude in their head, but that didn't prevent it from being formalized in a proof assistant. What they did was they just formalized the method for checking and then used that. You can similarly formalize the kind of reasoning that a model checker (or any other automated method) does and then use it in your proof assistant.

[pron]

> but the CompCert compiler is a highly non-trivial example of a program verified using dependent types, and which would not really be possible using automated methods.

First of all, it wasn't really verified using dependent types; it was verified in Coq. Coq's theory is, indeed, based on dependent types, but Coq is used more like a traditional proof assistant (HOL or TLA+) than a dependently typed programming language like Agda or Idris.

Second, CompCert, while certainly non-trivial, is also about 1/5 the size of jQuery, which means it's at least one to two orders-of-magnitude away from the average business application.

> You can similarly formalize the kind of reasoning that a model checker (or any other automated method) does and then use it in your proof assistant.

Yes. In the few cases where deductive proofs are used in industry, they're often used to tie together results from model checking.

[ghettoimp]

> We do it all the time. Whatever it is that you want your program to do, and any interesting functional property of it, is a non-compositional property. I know that because if it were compositional, you wouldn't need to write the program.

I don't think I understand what you're saying here?

Say I want to write a program that tells me the duplicated members of a list. My program might call helper routines like, "stable sort the list," and then "collect adjacent duplicates."

I might want to prove my program is "correct", e.g., a statement like, "the output is a list that contains exactly those elements of the input list whose duplicity exceeds 1"). To do this, I can first reason about the helper functions in isolation, then compose these results about the helper functions to establish that my desired property.

Why is this not an interesting property, or a program that I don't need to write?

[pron]

> Why is this not an interesting property, or a program that I don't need to write?

It's both of those things, but it's not compositional, because "finds duplicate members in a list" is not a property of either of your components. If it were a property of one of them, you wouldn't need the other.

All proofs proceed in stages, and "compose" known facts. But that's not the meaning of compositional, and the fact that the property you want easily arises from the properties of the component is luck. I gave an example on this page where this is not the case (the `foo bar` example), and it is provably not the case in general.

[ghettoimp]

Thanks. I think we may differ in our understanding of "compositional."

My understanding of "compositional" reasoning is something like, an approach where we (1) establish some properties about our helper functions, and then (2) reason about larger functions using these properties, instead of the definitions of the helper functions.

It seems like you have a different notion of compositional, which I'm still not sure I can articulate in a clear way... something more akin to transitivity?

[pron]

A property P is compositional with respect to terms A and B and composition ∘ if P(A) ∧ P(B) ⇔ P(A∘B); the equivalence is sometimes replaced with implication in one of the directions (this is a special case for a predicate, i.e. a boolean-valued function; a function F is compositional if F(A∘B) = F(A) ⋆ F(B)).

What you're saying is that proofs can be composed. That is true, but unhelpful, as it doesn't make proofs easy. All proofs work this way. Compositionality does (in fact, all properties that are easily proven by type inference are compositional; type safety itself is compositional). I've seen somewhere compositionality described as the opposite of emergence[1], which makes sense. A property is emergent in a composition if it is not a property of the components.

[1]: https://julesh.com/2017/04/22/on-compositionality/

[ghettoimp]

Thanks, this seems like a perfectly coherent definition of compositional. I think my earlier confusion was a purely terminological matter.

Regarding "What you're saying is that proofs can be composed. That is true, but unhelpful, as it doesn't make proofs easy." I agree that the ability to compose proofs does not make proof easy. But I would push back somewhat against the idea that this is unhelpful.

The ability to prove, in isolation, the relevant properties about some entity (e.g., a function, a hardware module, or what have you), and then to make use of these properties, without ever looking inside the entity again, to prove properties of some larger system, seems to me to be absolutely essential for scaling proofs to large systems.

This ability is of course completely common in tools like interactive proof assistants, but is less common in more automated procedures.

[pron]

> The ability to prove, in isolation, the relevant properties about some entity (e.g., a function, a hardware module, or what have you), and then to make use of these properties, without ever looking inside the entity again, to prove properties of some larger system, seems to me to be absolutely essential for scaling proofs to large systems.

I understand the motivation, and of course you're right that it would be "essential", it's just that it has been mathematically proven (see my post) that this is not the case. Results in computational complexity theory, that studies how hard it is to do things, show that "making use of these properties, without ever looking inside the entity again" does not, in fact, make verification easier. More precisely, the difficulty of proving a property of A_1 ∘ ... ∘ A_n is not any function of n, because we cannot hide the inner details of the components in a way that would make the effort lower even though that is what we want to do and even though it is essential for success.

In practice, we have not been able to scale proofs to large systems, which means that maybe there is some truth to those mathematical results.

[lmm]

> This is insufficient for a useful formalization of a program, because correctness properties aren't compositional, meaning that, in general, a sound specification of a program component would either be insufficient or unhelpful (i.e. no easier than the code itselg) for the writing of other components. Sure, in some cases it can be, but those are usually the easy cases. We need help with the hard ones.

Or we need to transform the hard cases into easy ones, which is what the whole dependent typing project is about: turning program correctness into just a matter of type safety, at which point it is just compositional. Maybe there are important cases that we can't solve this way, but I've not encountered any yet.

> But what you should be asking is this: as there haven't been any major relevant breakthroughs in formal logic in the past couple of decades, nor in any relevant proof techniques (we still use deduction for safety properties), our deductive proof capabilities aren't significantly higher now than they were 30 years ago. If it's all a matter of discipline, then, how come we're still not able to affordably (or at all, if the programs are not tiny) verify programs with deductive proofs?

I think the article itself is a pretty direct answer to this, in as much as it outlines the programme of work that's necessary to enable us to use these techniques in practical programs with more interesting propositions. I'd argue that we already do huge amounts of program verification with deductive proofs - that is, typechecking - many orders of magnitude more code is typechecked than has any other formal method applied - and the frontier of progress is how much we can represent important program properties within that. In terms of theoretical proof techniques, the dependent Haskell type system is indeed much the same as, say, the Java type system. But in terms of what properties are practical to encode and verify that way, the dependent Haskell type system is streets ahead. We've only had practical dependent-typed languages very recently - arguably we still don't. And many of the techniques for encoding important properties in our type systems (whether dependent or not) are also relatively new (e.g. the monadic region papers are relatively recent).

> the last thing you want is a rich specification language that forces you to use a particular verification technique, and that's exactly what dependent types do. You want to specify whatever helps you, and then you want to verify using whatever technique you need or can afford, to reach the appropriate level of cost/benefit for your requirements.

Assuming that we do always have an escape hatch, I don't see that using types forces anything any more than any other approach to specification? If I want to prove a larger overall proposition using types then of course I have to express any smaller propositions that I depend on in the language of types (as would be the case with any proof technique - there's no getting away from needing to express our premises and conclusions), but I still have the freedom to verify that smaller proposition using any technique or none.

[pron]

> Turning program correctness into just a matter of type safety, at which point it is just compositional.

It isn't. "Truth-preservation" in all deduction systems is also compositional (if the premises are true, so is the conclusion); that doesn't make the propositions compositional with respect to program components (if I conclude that X > 3 and Y > 2, then I can also conclude that X + Y > 5; the conclusion preserves the truth of the premises, not the property itself, as neither X nor Y is greater than 5). If you have a property of a program that isn't a property of a component, then the property is not compositional (note that type safety is: A∘B is type-safe iff A and B are; but type safety here is merely the inference step, similar to truth preservation). If it's not compositional, it can be arbitrarily hard to prove.

> Maybe there are important cases that we can't solve this way, but I've not encountered any yet.

If you're able to affordably prove any correctness property of any real-world program, this knowledge is worth billions. I am not aware of anyone who's ever made a similar claim.

> I'd argue that we already do huge amounts of program verification with deductive proofs - that is, typechecking - many orders of magnitude more code is typechecked than has any other formal method applied - and the frontier of progress is how much we can represent important program properties within that.

But the properties proven are easy. It's like saying, I can jump 50cm, so jumping all the way to the moon is just a matter of degree. No. There are real, fundamental, theoretical barriers between proving compositional properties and non-compositional ones (or those that require one or two inferences and ones that are more); between proving properties with zero or one quantifier, and properties with two quantifiers.

Also, while you can be pleased with Haskell's formal accomplishments, have you compared them to those of model checking in safety-critical real-time systems? Because once you do, you realize it doesn't look so good in comparison.

And your comparison of Haskell and Java is particularly interesting. You say that Haskell's type systems is "streets ahead". I agree (although I think this comes at a great cost). However, Haskell correctness or development cost is not "streets ahead" or even noticeably ahead. This shows that strengthening some deductive property is no guarantee to improving quality. Why? Because software correctness is very complicated. Its theory is complicated, and its practice is even more complicated.

> I don't see that using types forces anything any more than any other approach to specification

I think depdedent types are just redundant. You can get all or most of what give you without the inflexibility and the bad default using other means.

But look, I'm personally not too fond of dependent types in particular and deductive proofs in general, and consider them something you use when all else fails, and you have the money to spare. Others can be as bearish on model checking or concolic testing, paths that I think are more promising and I believe are seeing a bigger research investments. But what is certain is that no one has any idea whether we will find a way to drastically increase software correctness in the next twenty years, let alone which method will get us there. The one thing you can be sure of anyone who tells you they do is that they are simply unfamiliar with the different avenues explored or with many of the challenges involved (including social challenges).

[lmm]

> And your comparison of Haskell and Java is particularly interesting. You say that Haskell's type systems is "streets ahead". I agree (although I think this comes at a great cost). However, Haskell correctness or development cost is not "streets ahead" or even noticeably ahead.

I'd argue correctness is in fact streets ahead: orders of magnitude fewer defects (in terms of the code not doing what the programmer intended; the programmer not understanding what some other human intended is still as big a problem as ever) in practice. It's interesting how little value that actually brings in ordinary commercial development, but the correctness techniques will be there when the industry is ready for them. Development cost is much harder to measure; I'd argue that some systems developed with Haskell-like type systems would simply not have been possible to make without them, but that's the sort of question that's very difficult to answer objectively.

[pron]

> orders of magnitude fewer defects (in terms of the code not doing what the programmer intended; the programmer not understanding what some other human intended is still as big a problem as ever) in practice.

I don't see that, and I'm not aware of any report that reports that.

> It's interesting how little value that actually brings in ordinary commercial development, but the correctness techniques will be there when the industry is ready for them.

Except that in some cases it's already true. Companies like Amazon and Microsoft are seeing great value in using TLA+ and other formal methods, and now management encourages engineers to use them. I just don't see it for Haskell. Facebook is a good example, as they invest a lot in correctness research (both formal methods, like Infer, as well as inductive methods for automatic bug fixing and codegen[1]) and they also use some Haskell. But they're pushing hard on formal and inductive methods, but not so much on Haskell. I don't think correctness is a problem that cannot be addressed, and I believe there are techniques that address it. I just don't see that Haskell is one of them.

> Development cost is much harder to measure; I'd argue that some systems developed with Haskell-like type systems would simply not have been possible to make without them, but that's the sort of question that's very difficult to answer objectively.

You cannot claim that your technique is important and at the same time that it's effects are hard to see. I addressed that here: https://news.ycombinator.com/item?id=20718734

[1]: https://youtu.be/9QvcUNBPw4A https://youtu.be/2WIwx02t4PQ

[permeakra]

>I just don't see it for Haskell.

https://gitlab.haskell.org/ghc/ghc/wikis/team-ghc Facebook and Microsoft do see value in Haskell.

[pron]

Sure, Haskell's perfectly fine. But so are most of the popular languages, and those companies see more value in those.