4 ms·

>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

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

YorkshireSeason 5y 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.

YorkshireSeason 5y 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.