undefined | Better HN

0 pointsImprobableTruth4y ago0 comments

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

0 comments

3 comments · 1 top-level

YorkshireSeason4y ago· 2 in thread

> Take the spec for all sorting algorithms (giving observational equivalence):

It's not that simple. You also have to specify the effect set of the algorithm, meaning, assuming we do in place sort: every memory cell other that the input array are unchanged after termination. (If you return a fresh array, you have to specify something related). You also have to specify what happens for general sorting predicates, for example if the sorting predicate prints out the element it compares then this reveals (much of) the algorithm.

> The compression is stripping away the 'how'

The sorting example shows that this largely doesn't work in practise. In my experience for non-trivial programs you tend to have to carry around invariants whose complexity matches the size of the program you are verifying.

> I'm convinced that larger scale proof automation is way more essential than HoTT.

I strongly agree, but currently this proof automation is largely a hope, rather than a reality.

> crazy type hackery as seen in Haskell or Scala

Haskell and Scala have (local) type-inference. That makes those complex types (somewhat) digestible.

> dependent types just for refinement

If / when this really works well, so that you don't pay a price when you are not using complex types, then this would be very nice. I don't think PL technology is there yet. (I'm currently using a refinement typing approach in production code.)

ImprobableTruthOP4y ago

>It's not that simple. You also have to specify the effect set of the algorithm, meaning, assuming we do in place sort

I implicitly assumed that state would be encapsulated, since after all dependent types are fundamentally incompatible with observable state, but you're right that this is part of the spec. However I have severe doubts about the usability of any specification language that takes more than a one-liner to specify this.

>You also have to specify what happens for general sorting predicates

If you want to admit more general sorting predicates, sure, but normally you'd just allow pure functions.

>The sorting example shows that this largely doesn't work in practise. In my experience for non-trivial programs you tend to have to carry around invariants whose complexity matches the size of the program you are verifying.

If you include lemmas derived from the spec then I'd agree, but then the spec you have to check would still be a lot smaller. If not, then the only specs where I've experienced anything close to this are ones that are just the operational semantics of existing programs i.e. cases where you want to analyze a specific program. Otherwise I'm frankly uncertain as to what even the point of giving a spec would be.

>Haskell and Scala have (local) type-inference. That makes those complex types (somewhat) digestible.

Might make it more tractable to use, but I find my issue is that it's less direct and often obfuscates the meaning.

YorkshireSeason4y ago

> doubts about the usability of any specification language that ...

You can extrude hidden state in ML-like languages, which gives rise to all manner of subtle behaviour in combination with higher-order functions. As Pitts, Odersky, Stark and others have shown in the early 1990s, even just the ability to generate fresh names (in ML-like languages, this corresponds to the type Ref(Unit)), in conjunction with higher-order functions gives you essentially all the specification and reasoning problems of state.

> normally you'd just allow pure functions.

This is way too restrictive for non-trivial programs. This restriction work for sorting. And in reality even there you'd run into problem, for example if you take into account that a predicate might throw an exception (which, in practise you cannot avoid, think overflow or taking the head of an empty list).

> the only specs where I've experienced anything close to ...

I think that's because you have not attempted to prove substantial theorems about substantial code. The SeL4 verification is interesting in this context: it's specification (a purely functional specification of the OS behaviour) had, IIRC about 1/3 of the size of the OS's C code. Which is not much of a compression.

j / k navigate · click thread line to collapse