5 ms·

>your programs evolve very rapidly. Since with dependent types you loose type-inference, you now what to evolve two programs rather than one. Yes, just like yo

>your programs evolve very rapidly. Since with dependent types you loose type-inference, you now what to evolve two programs rather than one. Yes, just like you have to evolve your specification/documentation. Similarly, in the exploratory phase you'll stick to very 'rough' typing and next to no proofs and as the program gets clearer and solidifies, you can continuously refine your types (with the amount of refinement depending on how much certainty one wants). A mature program with a rigid spec is going to be harder to change, but that's just how it is anyway. >Moreover proofs are non-compositional: you make a tiny change somewhere and you might have to change all proofs. People on HN keep repeating this, but it's trivial because it's actually just a statement about the nature of properties. Proven invariants provide an interface to be used by the rest of the program. If the changes you make don't break your invariants but only the proofs, then you just have local adjustments to make. If your change cascades through the entire program, then it's because all the invariants get invalidated and your 'tiny' change actually changes a good deal about the semantics (and thus the spec) of the program. The exact same thing applies to unit tests, but you don't see people constantly bemoan the non-compositional nature of unit tests even though a 'tiny' change could break all your unit tests. >After all, your specification is just as likely to be buggy as your implementation code. Not only are specifications declarative, they're generally magnitudes smaller. If you're as confident in your spec as in your code, something is very, very wrong with your spec. Well, or your code is your spec, but in that case you get what you pay for.

YorkshireSeason 5y ago
> just like you have to evolve your specification/documentation. That is correct, and also one of the core reasons why in the vast majority of cases either no specification/documentation exists, or will only cover a small case of the actual specification. For example I would bet money that not a single function in the C, C++, Java and Python standard libraries is fully specified, in the sense of nailing down the program up to observational equivalence. (Aside: I can still count the programmers who would be able to sketch the observational equivalence using in e.g. C++.) > If your change cascades through the entire program, then it's because all the invariants get invalidated and your 'tiny' change actually changes a good deal about the semantics (and thus the spec) of the program. This is not borne out in practise. A lot of code refactoring I've done was trivial (e.g. changing the order or arguments), but ripples through the program and proof structure. HoTT was invented in order to automate some of those trivialities. Java exception specifications are an example: you call a different library function somewhere and need to change all exceptions specs up to the main function, rippling through millions of LoCs. That's why exception specs were abandoned. Another example are termination proofs (note that a full specification must involve termination proofs, which is why the existing expressive type theories don't give you unrestricted recursion, and also the reason why program logics are typically only for partial correctness). In my experience, termination bugs are rare, and it would be insanely counterproductive if I had to refactor all proofs globally just because I've made a slight change to some printf somewhere in a large code base. > unit tests, but you don't see people constantly bemoan The reason is that no programming language forces you to do unit tests. In contrast, expressive type-theories constantly force you to prove a lot of trivialities. > declarative, they're generally magnitudes smaller. I don't know what you mean by declarative (other than: leaving out some detail). But they cannot be smaller in general: if every program P had a full specification S that was shorter (here full specification means specifying P up to chosen notion of observational equivalence) then you've an impossibly strong compressor which you can use to prove that every string can be compressed even more. Contradiction. What you see in practise is that you only specify some properties of the program you are working on. For example sorting routines in C, C++, Java etc. I have never seen a specification that says what happens when the sorting predicate is nicely behaved (e.g. returns a < b on first call but a > b on second). It's fine to omit details, but that limits the correctness you get from your spec (and also limits program extraction). Moreover, if you only work with a partial specification, you can ask the question: what level of partiality in my specification gives me the best software engineering results. My personal and anecdotal experience (which includes dependently typed languages) has consistently been that the full automation given by let-polymorphism is the sweet spot for non-trivial programs (lets say > 10k LoC).
- ImprobableTruth 5y ago
  >the core reasons why in the vast majority of cases either no specification/documentation exists I feel that is much too pessimistic. >will only cover a small case of the actual specification. If the same applies to proofs: so be it. Don't let perfect be the enemy of good! >For example I would bet money that not a single function in the C, C++, Java and Python standard libraries is fully specified, in the sense of nailing down the program up to observational equivalence. I'd imagine so as well, but I think that's more indicative of how even a (superficially) simple language like C is not all that amenable to specification. > A lot of code refactoring I've done was trivial (e.g. changing the order or arguments), but ripples through the program and proof structure. This is not my experience. If you use sufficient proof automation, something like this should have next to no impact on proof structure. Univalence is useful, but a lot of refactoring is not just switching to isomorphic representations, so I'm convinced that larger scale proof automation is way more essential than HoTT. > Java exception specifications I'm not convinced that this is fundamental to specifying exceptions rather than just Java having particularly poor ergonomics for it. I've never met a person that actually liked implicit exceptions and if you ask people who dislike exceptions, that's often one key part of it. > In contrast, expressive type-theories constantly force you to prove a lot of trivialities. For all large dependently typed languages that actually bill themselves as programming languages (Agda, Idris, Lean) there is some sort of 'unsafe' feature that allows you to turn the termination checker off - at your own peril of course. But you only pay for what you use, if you don't need the additional correctness, you don't need to put in any more work, just like with unit tests. (There are also ways to safely defer termination proofs, but to be fair the experience isn't the best currently.) >I don't know what you mean by declarative (other than: leaving out some detail). Specs tell you the what but not (necessarily) the how. Take the spec for all sorting algorithms (giving observational equivalence): 1. The output list is a permutation of the input 2. The output is sorted in regards to some predicate. That's a couple lines at most (or a one-liner if you don't count the building blocks like the definition of a permutation), which is a good amount shorter and easier to verify than e.g. a full heapsort implementation. >But they cannot be smaller in general: if every program P had a full specification S that was shorter [...] then you've an impossibly strong compressor The compression is stripping away the 'how', that's why you can't 'write a spec for a spec' and compress further. >What you see in practise is that you only specify some properties of the program you are working on. Sure, writing a fully specified program of non-trivial size is currently really only possible if you're willing to ~waste~ invest a decade or more. >Moreover, if you only work with a partial specification, you can ask the question: what level of partiality in my specification gives me the best software engineering results. Why would you assume that there is a single level of partiality that gives the best results? I agree that HM style types are a great fit for 'general' programming because it has such low impedance, however I also believe that most programs have some areas where they would benefit from more specification. (I think people have a clear desire for this and that it's at least partially responsible for some of the crazy type hackery as seen in Haskell or Scala, which could often be greatly simplified with a richer type system.) Having a richer type system doesn't mean that you always have to fully use it. It's perfectly possible to just use a HM style/System F fragment. Using dependent types just for refinement is already one of the dominant styles for verification. If dependent types ever become mainstream in any way, I imagine it will also be largely in that style.

YorkshireSeason 5y ago

> just like you have to evolve your specification/documentation. That is correct, and also one of the core reasons why in the vast majority of cases either no specification/documentation exists, or will only cover a small case of the actual specification. For example I would bet money that not a single function in the C, C++, Java and Python standard libraries is fully specified, in the sense of nailing down the program up to observational equivalence. (Aside: I can still count the programmers who would be able to sketch the observational equivalence using in e.g. C++.) > If your change cascades through the entire program, then it's because all the invariants get invalidated and your 'tiny' change actually changes a good deal about the semantics (and thus the spec) of the program. This is not borne out in practise. A lot of code refactoring I've done was trivial (e.g. changing the order or arguments), but ripples through the program and proof structure. HoTT was invented in order to automate some of those trivialities. Java exception specifications are an example: you call a different library function somewhere and need to change all exceptions specs up to the main function, rippling through millions of LoCs. That's why exception specs were abandoned. Another example are termination proofs (note that a full specification must involve termination proofs, which is why the existing expressive type theories don't give you unrestricted recursion, and also the reason why program logics are typically only for partial correctness). In my experience, termination bugs are rare, and it would be insanely counterproductive if I had to refactor all proofs globally just because I've made a slight change to some printf somewhere in a large code base. > unit tests, but you don't see people constantly bemoan The reason is that no programming language forces you to do unit tests. In contrast, expressive type-theories constantly force you to prove a lot of trivialities. > declarative, they're generally magnitudes smaller. I don't know what you mean by declarative (other than: leaving out some detail). But they cannot be smaller in general: if every program P had a full specification S that was shorter (here full specification means specifying P up to chosen notion of observational equivalence) then you've an impossibly strong compressor which you can use to prove that every string can be compressed even more. Contradiction. What you see in practise is that you only specify some properties of the program you are working on. For example sorting routines in C, C++, Java etc. I have never seen a specification that says what happens when the sorting predicate is nicely behaved (e.g. returns a < b on first call but a > b on second). It's fine to omit details, but that limits the correctness you get from your spec (and also limits program extraction). Moreover, if you only work with a partial specification, you can ask the question: what level of partiality in my specification gives me the best software engineering results. My personal and anecdotal experience (which includes dependently typed languages) has consistently been that the full automation given by let-polymorphism is the sweet spot for non-trivial programs (lets say > 10k LoC).

ImprobableTruth 5y ago
>the core reasons why in the vast majority of cases either no specification/documentation exists I feel that is much too pessimistic. >will only cover a small case of the actual specification. If the same applies to proofs: so be it. Don't let perfect be the enemy of good! >For example I would bet money that not a single function in the C, C++, Java and Python standard libraries is fully specified, in the sense of nailing down the program up to observational equivalence. I'd imagine so as well, but I think that's more indicative of how even a (superficially) simple language like C is not all that amenable to specification. > A lot of code refactoring I've done was trivial (e.g. changing the order or arguments), but ripples through the program and proof structure. This is not my experience. If you use sufficient proof automation, something like this should have next to no impact on proof structure. Univalence is useful, but a lot of refactoring is not just switching to isomorphic representations, so I'm convinced that larger scale proof automation is way more essential than HoTT. > Java exception specifications I'm not convinced that this is fundamental to specifying exceptions rather than just Java having particularly poor ergonomics for it. I've never met a person that actually liked implicit exceptions and if you ask people who dislike exceptions, that's often one key part of it. > In contrast, expressive type-theories constantly force you to prove a lot of trivialities. For all large dependently typed languages that actually bill themselves as programming languages (Agda, Idris, Lean) there is some sort of 'unsafe' feature that allows you to turn the termination checker off - at your own peril of course. But you only pay for what you use, if you don't need the additional correctness, you don't need to put in any more work, just like with unit tests. (There are also ways to safely defer termination proofs, but to be fair the experience isn't the best currently.) >I don't know what you mean by declarative (other than: leaving out some detail). Specs tell you the what but not (necessarily) the how. Take the spec for all sorting algorithms (giving observational equivalence): 1. The output list is a permutation of the input 2. The output is sorted in regards to some predicate. That's a couple lines at most (or a one-liner if you don't count the building blocks like the definition of a permutation), which is a good amount shorter and easier to verify than e.g. a full heapsort implementation. >But they cannot be smaller in general: if every program P had a full specification S that was shorter [...] then you've an impossibly strong compressor The compression is stripping away the 'how', that's why you can't 'write a spec for a spec' and compress further. >What you see in practise is that you only specify some properties of the program you are working on. Sure, writing a fully specified program of non-trivial size is currently really only possible if you're willing to ~waste~ invest a decade or more. >Moreover, if you only work with a partial specification, you can ask the question: what level of partiality in my specification gives me the best software engineering results. Why would you assume that there is a single level of partiality that gives the best results? I agree that HM style types are a great fit for 'general' programming because it has such low impedance, however I also believe that most programs have some areas where they would benefit from more specification. (I think people have a clear desire for this and that it's at least partially responsible for some of the crazy type hackery as seen in Haskell or Scala, which could often be greatly simplified with a richer type system.) Having a richer type system doesn't mean that you always have to fully use it. It's perfectly possible to just use a HM style/System F fragment. Using dependent types just for refinement is already one of the dominant styles for verification. If dependent types ever become mainstream in any way, I imagine it will also be largely in that style.