7 ms·

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

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.

dwohnitmok 7y ago
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.
- chrisdone 7y ago
  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!
- pron 7y ago
  > 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.html 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.
  - dwohnitmok 7y ago
    > 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)

dwohnitmok 7y ago

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.

chrisdone 7y ago
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!
pron 7y ago
> 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.html 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.
- dwohnitmok 7y ago
  > 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)