Hacker News Reader

Comment by yaseer | Hacker News Reader

I think the line of reasoning is incorrect.

Most mathematical arguments are actually not formal, in the way a program is a formal language.

In many instances, there are not only ambiguities but errors in the mathematical expression. They only become formalised to an equivalent degree in a system like Isabelle or Coq.

Writing proofs in Isabelle and Coq is essentially the same process as writing highly functional code, and is susceptible to the same arduous process. It's hard because it's a formal language running on a rigid machine.

Programming would be easy if you specified everything in a semi --formal pseudo code, designed to be interpreted by a human mind that can fill in the blanks. This is what most mathematics is.

View on HN

Yeah, definitely. Math proofs are above all else about being just rigorous enough to convince other people that the proof is correct, at least in the sense that small mistakes or oversights don't destroy the overall validity of the proof. That is, the idea is sound even if all the steps aren't 100% rigorous. And I don't mean to belittle; programs are similarly meant for other people to read and understand, but with the additional restriction that they have to be formal and unambiguous enough for a machine to understand them too!

I often point out that exactly because of this, it's a red flag for me when I see a CS paper that relies on maths - it often indicates handwaving and missing details that would be a lot more obvious in code to the extent that I've learned to expect that if the paper is full of maths, chances are it will be a long, arduous process to try to reconstruct what the paper is actually doing. Often it extends to missing out essential details, such as values of important constants and the like.

Another similar vantage point is that that the math can have no relation to what's actually happening. For example, the author might indicate in one step they invert a matrix, but instead use some heavily regularized solver. It might be that only a few eigenmodes are invertible which changes the physics of the problem.

As someone who's worked a bit in theoretical CS, I think this is attributable to theory's different culture. In theory the focus tends to be more on intrinsic qualities of the problem in question -- does there exist a polynomial time solution? a sublinear time solution? how is it like or not like other problems? -- and less on clever engineering ways to optimize the constants in the problem, which is why the implementation (and its attendant constants) often seems like an afterthought.

This is more useful than it sounds, since studying problems themselves can often lead to generalizations ("ah, this is NP-hard") that let you import plug-and-play knowledge ("we shouldn't expect a polynomial time solution").

But yeah when it comes time to implement/simulate, papers that are hand wavey with constants get annoying.

I've seen this happen in papers that "just" presented something as simple as an image thresholding function where the exact code took less than a dozen lines of C once I'd reverse engineered from test data what the constant their method relied on that they'd unhelpfully left out.

The implementation in fact took less space than their plain English description...

For papers that are deeply abstract and focused on solving a problem of the nature you describe, that's to me very different, and clearly there are papers where you won't get around using maths to communicate the problem well. But at least in the fields I've worked in, those kind of papers are rare exceptions.

To be fair, CS theory is basically just mathematics :)

On the other hand, papers with actual code muddy the actual contribution of their paper with code to allocate data structures, specify number of threads, etc. The audience for a paper is people looking to understand a new algorithm.

I do wish more authors published their source code separately from the actual paper.

You don't need to present every little detail in the paper, but it very quickly becomes obvious what is missing.

This distinction was very obvious when I did the literature survey for my MSc. - the papers with even partial code fragments were uniformly less likely to miss out essential information.

Math being less precise than code does not make it automatically "hand wavy".

It doesn't have to be, but the way it's used in CS papers often is hand wavy, in that important details are often glossed over or left entirely out.

Can you link me an example or two of good CS papers that don't rely on math?

e2e argument:

http://web.mit.edu/Saltzer/www/publications/rfc/csr-rfc-185....

Unix:

https://people.eecs.berkeley.edu/~brewer/cs262/unix.pdf

or pretty much everything here: http://cseweb.ucsd.edu/classes/fa17/cse221-a/readings.html

CS can be pretty broad.

Most of Michael Franz' papers, for example:

http://www.michaelfranz.com/

To answer my own question, I came across this paper today which was I found quite insightful and had little to no math especially for a PLT paper:

Elementary Strong Functional Programming by D.A. Turner

https://pdfs.semanticscholar.org/b60b/1c2e49ec6f574f220f162c...

I've seen that a lot in applied computer science. For example, papers describing algorithms to compute measurements in 3d geometry with equations. Equations are almost completely useless when it is numerical stability and precision issues you need. 32 bit floating points have very little in common with the real numbers.

Reply on news.ycombinator.com