4 ms·

> Dependent types are not a verification technique...Deciding to encode program properties in dependent types (e.g. Idris) or direct logic (e.g. Java+JML) doesn

> Dependent types are not a verification technique...Deciding to encode program properties in dependent types (e.g. Idris) or direct logic (e.g. Java+JML) doesn't make verification any easier or harder. For what it's worth, every time I see articles and comments about the use of formal verification in general purpose programming around here, I never see any mention of how the actual verification part requires incredibly challenging manual proofs. In particular, I see articles about dependent types that give the impression you get the proofs for free when that isn't the case.

pron 11y ago
Let me respond to that with a quote from "No Silver Bullet, Refired", by another Turing Award winner, Fred Brooks: > Even if "NSB" were universally seen as pessimistic, what is wrong with that? Is Einstein's statement that nothing can travel faster than the speed of light "bleak" or "gloomy?" How about Godel's result that some things cannot be computed? "NSB" undertakes to establish that "the very nature of software makes it unlikely that there will ever be any silver bullets." Turski, in his excellent response paper at the IFIP Conference, said eloquently: >> Of all misguided scientific endeavours, none are more pathetic than the search for the philosophers' stone, a substance supposed to change base metals into gold. The supreme object of alchemy, ardently pursued by generations of researchers generously funded by secular and spiritual rulers, is an undiluted extract of wishful thinking, of the common assumption that things are as we would like them to be. It is a very human belief. It takes a lot of effort to accept the existence of insoluble problems. The wish to see a way out, against all odds, even when it is proven that it does not exist, is very, very strong. And most of us have a lot of sympathy for these courageous souls who try to achieve the impossible. And so it continues. Dissertations on squaring a circle are being written. Lotions to restore lost hair are concocted and sell well. Methods to improve software productivity are hatched and sell very well. All too often we are inclined to follow our own optimism (or exploit the optimistic hopes of our sponsors). All too often we are willing to disregard the voice of reason and heed the siren calls of panacea pushers. > Turski and I both insist that pipe-dreaming inhibits forward progress and wastes effort. > So we come back to fundamentals. Complexity is the business we are in, and complexity is what limits us. R. L. Glass, writing in 1988, accurately summarizes my 1995 views: >> So what, in retrospect, have Parnas and Brooks said to us? That software development is a conceptually tough business. That magic solutions are not just around the corner. That it is timefor the practitioner to examine evolutionary improvements rather than to wait—or hope—for revolutionary ones. >> Some in the software field find this to be a discouraging picture. They are the ones who still thought breakthroughs were near at hand. >> But some of us—those of us crusty enough to think that we are realists—see this as a breath of fresh air. At last, we can focus on something a little more viable than pie in the sky. Now, perhaps, we can get on with the incremental improvements to software productivity that are possible, rather than waiting for the breakthroughs that are not likely to ever come. --- So discussing some methods of formal verification (such as manually checking dependent types) as a solution is like saying a particle accelerator is the solution to the alchemist's problem. Theoretically it can work; in practice, it's often too much effort :) Personally I'm not sure pipe-dreams inhibit forward progress, but they sure do generate a lot of noise...
lmm 11y ago
I'm not convinced it is necessarily that challenging, because the proof goes with the code. A program source is already an informal proof of correctness - the reason we tend to believe our programs are correct is that their code looks like it does the correct thing. Few maintainable programs rely on invariants that appear "magically" out of nowhere; a human reader would believe an invariant held because they could see a code path or state that represented that invariant. I think for most real-world code, the theorem that the code represents (in a Curry-Howard sense) tends to be trivial.
- seanwilson 11y ago
  > I'm not convinced it is necessarily that challenging, because the proof goes with the code. A program source is already an informal proof of correctness - the reason we tend to believe our programs are correct is that their code looks like it does the correct thing. Few maintainable programs rely on invariants that appear "magically" out of nowhere; a human reader would believe an invariant held because they could see a code path or state that represented that invariant. Have you done any formal proofs before? You're severely underestimating how difficult and time consuming they are to do even if you do have some intuition about why they are correct. The sel4 microkernel took around 5 years for around 20 experts to verify for example. Verifying a program can result in you having to prove arbitrarily difficult maths theorems so it's similar to saying automating arbitrarily difficult maths theorems should be trivial. > I think for most real-world code, the theorem that the code represents (in a Curry-Howard sense) tends to be trivial. Yes, the theorem/specification statement may be trivial compared to the code but the hard part is coming up with the proof that shows the code matches the specification. You don't get this for free.
  - lmm 11y ago
    > Verifying a program can result in you having to prove arbitrarily difficult maths theorems so it's similar to saying automating arbitrarily difficult maths theorems should be trivial. But you wouldn't write a program that depended on a theorem that wasn't proven, no? I mean often the only mathematically hard parts of a given program are in the libraries it uses - which could ship with their own proofs. > Yes, the theorem/specification statement may be trivial compared to the code but the hard part is coming up with the proof that shows the code matches the specification. You don't get this for free. Doesn't the structure of the code tell you how to structure the proof though? Like, if you've written code that appends to a list by appending a single element and recursing, the way you prove it correct is to prove that it appends a single element and that it recurses correctly. If you've written something that's supposed to be a sorting algorithm and the code rearranges the elements of a list, why is it that you believe this particular rearrangement of the elements is a correct sort? Isn't the answer to that question your proof of correctness?

pron 11y ago

Let me respond to that with a quote from "No Silver Bullet, Refired", by another Turing Award winner, Fred Brooks: > Even if "NSB" were universally seen as pessimistic, what is wrong with that? Is Einstein's statement that nothing can travel faster than the speed of light "bleak" or "gloomy?" How about Godel's result that some things cannot be computed? "NSB" undertakes to establish that "the very nature of software makes it unlikely that there will ever be any silver bullets." Turski, in his excellent response paper at the IFIP Conference, said eloquently: >> Of all misguided scientific endeavours, none are more pathetic than the search for the philosophers' stone, a substance supposed to change base metals into gold. The supreme object of alchemy, ardently pursued by generations of researchers generously funded by secular and spiritual rulers, is an undiluted extract of wishful thinking, of the common assumption that things are as we would like them to be. It is a very human belief. It takes a lot of effort to accept the existence of insoluble problems. The wish to see a way out, against all odds, even when it is proven that it does not exist, is very, very strong. And most of us have a lot of sympathy for these courageous souls who try to achieve the impossible. And so it continues. Dissertations on squaring a circle are being written. Lotions to restore lost hair are concocted and sell well. Methods to improve software productivity are hatched and sell very well. All too often we are inclined to follow our own optimism (or exploit the optimistic hopes of our sponsors). All too often we are willing to disregard the voice of reason and heed the siren calls of panacea pushers. > Turski and I both insist that pipe-dreaming inhibits forward progress and wastes effort. > So we come back to fundamentals. Complexity is the business we are in, and complexity is what limits us. R. L. Glass, writing in 1988, accurately summarizes my 1995 views: >> So what, in retrospect, have Parnas and Brooks said to us? That software development is a conceptually tough business. That magic solutions are not just around the corner. That it is timefor the practitioner to examine evolutionary improvements rather than to wait—or hope—for revolutionary ones. >> Some in the software field find this to be a discouraging picture. They are the ones who still thought breakthroughs were near at hand. >> But some of us—those of us crusty enough to think that we are realists—see this as a breath of fresh air. At last, we can focus on something a little more viable than pie in the sky. Now, perhaps, we can get on with the incremental improvements to software productivity that are possible, rather than waiting for the breakthroughs that are not likely to ever come. --- So discussing some methods of formal verification (such as manually checking dependent types) as a solution is like saying a particle accelerator is the solution to the alchemist's problem. Theoretically it can work; in practice, it's often too much effort :) Personally I'm not sure pipe-dreams inhibit forward progress, but they sure do generate a lot of noise...

lmm 11y ago

I'm not convinced it is necessarily that challenging, because the proof goes with the code. A program source is already an informal proof of correctness - the reason we tend to believe our programs are correct is that their code looks like it does the correct thing. Few maintainable programs rely on invariants that appear "magically" out of nowhere; a human reader would believe an invariant held because they could see a code path or state that represented that invariant. I think for most real-world code, the theorem that the code represents (in a Curry-Howard sense) tends to be trivial.

seanwilson 11y ago
> I'm not convinced it is necessarily that challenging, because the proof goes with the code. A program source is already an informal proof of correctness - the reason we tend to believe our programs are correct is that their code looks like it does the correct thing. Few maintainable programs rely on invariants that appear "magically" out of nowhere; a human reader would believe an invariant held because they could see a code path or state that represented that invariant. Have you done any formal proofs before? You're severely underestimating how difficult and time consuming they are to do even if you do have some intuition about why they are correct. The sel4 microkernel took around 5 years for around 20 experts to verify for example. Verifying a program can result in you having to prove arbitrarily difficult maths theorems so it's similar to saying automating arbitrarily difficult maths theorems should be trivial. > I think for most real-world code, the theorem that the code represents (in a Curry-Howard sense) tends to be trivial. Yes, the theorem/specification statement may be trivial compared to the code but the hard part is coming up with the proof that shows the code matches the specification. You don't get this for free.
- lmm 11y ago
  > Verifying a program can result in you having to prove arbitrarily difficult maths theorems so it's similar to saying automating arbitrarily difficult maths theorems should be trivial. But you wouldn't write a program that depended on a theorem that wasn't proven, no? I mean often the only mathematically hard parts of a given program are in the libraries it uses - which could ship with their own proofs. > Yes, the theorem/specification statement may be trivial compared to the code but the hard part is coming up with the proof that shows the code matches the specification. You don't get this for free. Doesn't the structure of the code tell you how to structure the proof though? Like, if you've written code that appends to a list by appending a single element and recursing, the way you prove it correct is to prove that it appends a single element and that it recurses correctly. If you've written something that's supposed to be a sorting algorithm and the code rearranges the elements of a list, why is it that you believe this particular rearrangement of the elements is a correct sort? Isn't the answer to that question your proof of correctness?