Hacker News Reader

Comment by lincolnq | Hacker News Reader

Did you even read the article?

Edit: This is exactly what the author is arguing against. Yes, you're writing a proof, but that's not the point of what you're doing at all.

View on HN

I read the article and disagree. Computer science is a discipline of applied mathematics.

Saying that computer science is not mathematics because it involves real world complications, is like saying that experimental physics isn't physics because it is not done by theorists.

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.

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.

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.

Most interesting programs cannot be studied analytically.

That's a pretty strong statement. Care to provide some examples?

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.

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

Reply on news.ycombinator.com