4 ms·

Of course I've read it. He says just the foundations are math. He says actual programs (e.g. those implementing networking protocols) are not math. Curry and Ho

by zeteo 14y ago

Of course I've read it. He says just the foundations are math. He says actual programs (e.g. those implementing networking protocols) are not math. Curry and Howard beg to differ.

ArtB 14y ago
They can be interpreted as math, but they aren't really. If you are using Coq or something verified it can be, but especially when you are using a dynamic language and you have no idea of the types of objects that will be passed as parameters or when you are just slapdashing bits of scripts together (like, "hmm, that failed, maybe I should just +1 to it?") it's hard to compare that to the rigorous discipline called math.
- zeteo 14y ago
  Math went on for millenia without computerized proof checking and yes, some of those proofs were buggy. The difference between a professional mathematician and a software engineer is no more than that between a C and a Prolog programmer. Anyone who has written both proofs by induction and recursive programs can easily see the correspondence, even without the Curry-Haskell proof that the correspondence exists.
scott_s 14y ago
Most interesting programs cannot be studied analytically.
- cantankerous 14y ago
  That's a pretty strong statement. Care to provide some examples?
  - scott_s 14y ago
    You are correct that it's too strong. Most interesting programs cannot be fully studied analytically. The largest piece of software that has been proved correct is less than 10,000 lines of code. (Sadly, I have no reference for that - a recent speaker here talking about software testing made this claim with a reference that I have forgotten.) But real programs very quickly get to the point that it's impractical to fully understand them analytically. We have to execute them and observe their behavior.
    - cantankerous 14y ago
      Sorry if I seemed offensively skeptical, it wasn't my intent. I was wondering if I was missing something obvious ...which happens more than I'd like to think about. I agree with you on the lines of code. I think SeL4 is about 9,300 and I can't come up with something much longer (I don't think CompCert can really count because it's really just a lot of separate smaller programs running in succession, and generally one probably doesn't count Coq code as part of the program being verified, but everybody's got their own opinion).

by zeteo 14y ago

Of course I've read it. He says just the foundations are math. He says actual programs (e.g. those implementing networking protocols) are not math. Curry and Howard beg to differ.

ArtB 14y ago

They can be interpreted as math, but they aren't really. If you are using Coq or something verified it can be, but especially when you are using a dynamic language and you have no idea of the types of objects that will be passed as parameters or when you are just slapdashing bits of scripts together (like, "hmm, that failed, maybe I should just +1 to it?") it's hard to compare that to the rigorous discipline called math.

zeteo 14y ago
Math went on for millenia without computerized proof checking and yes, some of those proofs were buggy. The difference between a professional mathematician and a software engineer is no more than that between a C and a Prolog programmer. Anyone who has written both proofs by induction and recursive programs can easily see the correspondence, even without the Curry-Haskell proof that the correspondence exists.

scott_s 14y ago

Most interesting programs cannot be studied analytically.

cantankerous 14y ago
That's a pretty strong statement. Care to provide some examples?
- scott_s 14y ago
  You are correct that it's too strong. Most interesting programs cannot be fully studied analytically. The largest piece of software that has been proved correct is less than 10,000 lines of code. (Sadly, I have no reference for that - a recent speaker here talking about software testing made this claim with a reference that I have forgotten.) But real programs very quickly get to the point that it's impractical to fully understand them analytically. We have to execute them and observe their behavior.
  - cantankerous 14y ago
    Sorry if I seemed offensively skeptical, it wasn't my intent. I was wondering if I was missing something obvious ...which happens more than I'd like to think about. I agree with you on the lines of code. I think SeL4 is about 9,300 and I can't come up with something much longer (I don't think CompCert can really count because it's really just a lot of separate smaller programs running in succession, and generally one probably doesn't count Coq code as part of the program being verified, but everybody's got their own opinion).