> These steps are not guaranteed to be taken, they require discipline, time and process, and history has shown that steps with those requirements are only taken when absolutely necessary, not as a matter of course.
They require no more discipline than remembering to run your unit tests in your build. History has shown that people -- even ordinary programmers -- have come to incorporate their unit tests into their build so that they run automatically. A much, much bigger challenge would be to get programmers to write specifications in the first place -- whether in types or in logic.
> Firstly, you don't always, given type inference.
Those types that type inference can infer correspond to specs that automated tools prove. The algorithms are even the same.
> The proof just follows naturally from reasoning about the semantics of the code as they're writing it, not later when they have to go back and read it who-knows-how-much-later, and then figure out what conditions they should try to verify.
Whether you write your proofs using dependent types or using logic, the process is identical, and in either case it is so laborious that no one has been able to do it for large programs anyway, not before, not during and not after.
> You now have a mashup of formal properties with uncertain failure modes.
1. Those are not the same failure modes. 2. Welcome to the world of formal methods. Again, full proof of large programs has never been accomplished. We who use formal methods in real-world projects must use a mashup of techniques of various confidence levels.
> Tests aren't a meaningful form of verification; they can't prove the absence of bugs, only their presence. Rarely is a property verifiable by exhaustive case tests.
You sound like someone quoting something rather than a practitioner of formal methods. We use a plethora of tools, each contributing something to the confidence. We have no choice given that formal proof is beyond our reach for the properties that we must verify.
> They're writing everything in the same language, not different languages using different compilers and different tools.
No, those are different tools (compiler and test tool) and different languages (type level and object level; yes they use the same syntax, but code-level spec also does.
> Right, because dependent types typically leak too much of their implementation due to the properties that must be satisfied.
Dependent types are just a formalism for writing specifications. The problem is what kind of verification is done, and types require proof.
> Idris' syntactic support can then make this easy for library clients to use correctly.
No one has ever been able to make formal proofs even moderately hard, let alone easy. Maybe Idris will perform this miracle, but my bet is on other formal verification techniques. I am not aware of any formal methods researcher who believes that formal proofs will become affordable for mainstream software using any of the formal proof techniques we currently have.
> Of course, you can suggest this is all speculative, but it's not pie-in-the-sky as you've been claiming. People have been doing this for years already, with both dependent and ordinary type systems (see Oleg's lightweight static capabilities).
As someone who actually uses formal methods, I know what's been done and what's only been claimed in research. Lightweight static capabilites are not really formal methods; their tokens for runtime assertions. They're cool (and have been used in OOP languages since long before that paper), but they're something else altogether.
> because what are types if not a form of code-level specification?
That's right, but they're specs that settle for no weaker form of verification than proof.
> Code-level specifications that are not types tend to be fairly non-compositional...
Huh? It's just a different formalism. They behave the same, and require the same discipline. The only difference is that they don't necessarily require proof.
> More typical properties are the correctness of protocols, for which we might use session types, that a general ledger is always balanced, that resources are always cleaned up and so don't take down your service, and so on.
Session types are really weak, and can't actually verify interesting protocols. That resources are cleaned is a local property that doesn't fall in the category we're discussing (and can be achieved without formal methods at all). That a general ledger is always balanced -- well, that's a correctness property that I'd like to see someone prove in Idris in a real, large distributed system. It's never been successfully done.
> These are relatively simple properties for which we now have good, reusable abstractions
What we don't know is what is the relationship between having such weak guarantees and actual software correctness.
They require no more discipline than remembering to run your unit tests in your build. History has shown that people -- even ordinary programmers -- have come to incorporate their unit tests into their build so that they run automatically. A much, much bigger challenge would be to get programmers to write specifications in the first place -- whether in types or in logic.
> Firstly, you don't always, given type inference.
Those types that type inference can infer correspond to specs that automated tools prove. The algorithms are even the same.
> The proof just follows naturally from reasoning about the semantics of the code as they're writing it, not later when they have to go back and read it who-knows-how-much-later, and then figure out what conditions they should try to verify.
Whether you write your proofs using dependent types or using logic, the process is identical, and in either case it is so laborious that no one has been able to do it for large programs anyway, not before, not during and not after.
> You now have a mashup of formal properties with uncertain failure modes.
1. Those are not the same failure modes. 2. Welcome to the world of formal methods. Again, full proof of large programs has never been accomplished. We who use formal methods in real-world projects must use a mashup of techniques of various confidence levels.
> Tests aren't a meaningful form of verification; they can't prove the absence of bugs, only their presence. Rarely is a property verifiable by exhaustive case tests.
You sound like someone quoting something rather than a practitioner of formal methods. We use a plethora of tools, each contributing something to the confidence. We have no choice given that formal proof is beyond our reach for the properties that we must verify.
> They're writing everything in the same language, not different languages using different compilers and different tools.
No, those are different tools (compiler and test tool) and different languages (type level and object level; yes they use the same syntax, but code-level spec also does.
> Right, because dependent types typically leak too much of their implementation due to the properties that must be satisfied.
Dependent types are just a formalism for writing specifications. The problem is what kind of verification is done, and types require proof.
> Idris' syntactic support can then make this easy for library clients to use correctly.
No one has ever been able to make formal proofs even moderately hard, let alone easy. Maybe Idris will perform this miracle, but my bet is on other formal verification techniques. I am not aware of any formal methods researcher who believes that formal proofs will become affordable for mainstream software using any of the formal proof techniques we currently have.
> Of course, you can suggest this is all speculative, but it's not pie-in-the-sky as you've been claiming. People have been doing this for years already, with both dependent and ordinary type systems (see Oleg's lightweight static capabilities).
As someone who actually uses formal methods, I know what's been done and what's only been claimed in research. Lightweight static capabilites are not really formal methods; their tokens for runtime assertions. They're cool (and have been used in OOP languages since long before that paper), but they're something else altogether.
> because what are types if not a form of code-level specification?
That's right, but they're specs that settle for no weaker form of verification than proof.
> Code-level specifications that are not types tend to be fairly non-compositional...
Huh? It's just a different formalism. They behave the same, and require the same discipline. The only difference is that they don't necessarily require proof.
> More typical properties are the correctness of protocols, for which we might use session types, that a general ledger is always balanced, that resources are always cleaned up and so don't take down your service, and so on.
Session types are really weak, and can't actually verify interesting protocols. That resources are cleaned is a local property that doesn't fall in the category we're discussing (and can be achieved without formal methods at all). That a general ledger is always balanced -- well, that's a correctness property that I'd like to see someone prove in Idris in a real, large distributed system. It's never been successfully done.
> These are relatively simple properties for which we now have good, reusable abstractions
What we don't know is what is the relationship between having such weak guarantees and actual software correctness.