Why is writing mathematical proofs more fault-proof than writing code? (2011) | Hacker News Reader

Why is writing mathematical proofs more fault-proof than writing code? (2011)

cs.stackexchange.com

238 pointsdgellow132 comments

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.

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.

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!

Because in mathematical proofs the preconditions are usually explicit and well understood. A program usually has reality-bound constraints that are not explicit, e.g. "does not work unless the target system has at least 3.5mb of memory" or "assumes that opcode X never fails" or "assumes memory is consistent and never is corrupted"

Programs could be explicit about those constraints, encode more of them statically and check them statically.

Everything has a failure rate. This introduces another set of heuristics (and another false-{positive,negative} rate), another set of potential implementation bugs in those heuristics. What if being able to run the program on a particularly memory-limited computer could save the universe, even more slowly than the project manager originally wanted it to run?

Statically encoding something like a memory constraint sounds very hard for all but the simplest algorithms. What about a randomized algorithm that sometimes uses more heap? How do you get around not knowing how much it's going to use without running it?

Allocate for the worst case use in the bss. The program's static size indicates explicit memory requirements.

That's Design-by-Contract. On checking side, one can generate tests from specs, static analysis, turn them plus code into verification conditions to feed to solvers, or inputs to theorem prover for handling complex stuff. Eiffel implements DbC with test generation. SPARK Ada does automated and manual proofs. Ada 2012 added contracts but idk tool support. Many languages have ways of emulating this functionality, too.

What you're describing is essentially a proven, lightweight, formal method for improving software quality. Many commercial apps use it.

indeed, very few programming languages actually do that, and you're probably running the language on top of another language that has flawed guarantees on those constraints. Or hardware. How do you guarantee your program hasn't gone rogue if you can't guarantee the bits in your memory.

Yeah, this would be the question for fault tolerance and the whole world of distributed systems that inevitably comes with it.

i think the reasons pointed out in the post and many comments here on HN are more of the cause,

but another reason is that code often has to be written in a shorter time frame. there are tools like coq that enable people to write code that is correct by proofs, but I'd hate to do my daily work that way

I consider myself a bit of an expert in this area, I work on lots of mathematical algorithms.

My experience is this isn't true. The reason it seems to be true is mathematicians will skip over writing out "boring" edge cases, which while hypothetically simple are often where the bugs occur in code.

From the people I've talked to it gets even worse than this when you cross domain or language barriers too. There are all kinds of implicit assumptions about variables that can get used in subtly different ways by convention, which were you to spell out said assumptions, you'd have a whole lot more places where bugs can occur in code.

There are many, many errors in the published mathematical literature, and the older you get, the more of them you see. What I find even more amusing is when people don't withdraw their papers after you convince them their paper is fundamentally wrong, and they agree the argument can't be salvaged. I used to think of mathematical arguments that I couldn't follow as being "advanced" and written by "elite" people. I now consider them "heuristic" or worse still, "the spam of confused minds".

At the top of various fields, you basically have a bunch of experts writing for each other, using heuristic arguments, and writing only to a level that will convince one another that the result is "probably true". Important results of great public interest are picked to pieces. But this is not true of less prominent work (of which the majority of the literature consists), probably each paper is read an average of 0.6 times, including by the authors and referees.

> There are many, many errors in the published mathematical literature, and the older you get, the more of them you see.

Can you provide any examples? I know this is true, but I'm interested in examples you have off the top of your head.

For the most part, I'd prefer not to give explicit examples, since it amounts to public shaming of (often) still living authors.

In broad generality, I work on algorithms for number theory and fast arithmetic. If you look at published, peer reviewed, conference proceedings in this area, there are many, many well known cases of incorrect algorithms.

Sometimes in the mathematical literature there are multiple definitions given for similar concepts, and later authors assume without checking that they are the same thing. I'm aware of papers that are entirely wrong because of this.

Another area where errors are common is in stating identities, which the author didn't try to check with a computer.

But, I am also aware of examples in less computational, pure mathematics too.

The phenomenon also extends to famous textbooks and undergraduate notes. Simply look at the errata section of any sufficiently well-read textbook. Sometimes incorrect or inadequate assumptions are carried right through the book without explicitly mentioning them.

A famous cryptographer used to have online a rant about half-gcd algorithms. As the story goes, the original publication was correct. One famous improvement is only correct for polynomials. A later attempt by another author is not correct for polynomials or integers. And a famous textbook in the field took until their third edition to get the proof/algorithm correct.

I've even seen an incorrect definition given for something as fundamental as a field, even by the most famous of mathematicians, now two or three times I think (admittedly once by someone who wasn't an algebraist).

You can find many examples easily by Googling, "proof was unfortunately incorrect", although it is usually stated more generously than that, e.g. "we have been unable to reconstruct their argument", "we supply some missing details", "it is not clear exactly what the authors intended", "where we correct an obvious typographical error", etc.

And this is to say nothing of the almost infinite supply of papers that are missing critical elements of the proof, or where folklore theorems are relied upon without proof or citation. Simply search for the ubiquitous phrases, "the well-known result" and "it is well-known that".

Nice observation.

What really matters is the actual thinking about the actual subject. In nearly all math proofs, the writing is closer to that thinking than in coding. Or, each sentence in a math proof -- and well written proofs actually are written in sentences -- is closer to the thinking than for the programming language statements in the coding. Or, look at the statements in the coding -- without mnemonic identifier naming, they are close to just gibberish.

To get the coding closer to the thinking, that's the documentation in the coding. However the documentation is usually not as precise as the sentences in a math proof or the statements in code.

So, maybe we need to do something to get programming closer to the real thinking: For this, maybe try to have what we use in programming to be easier to describe. That is, in a math proof, we have numbers, sets, vectors, functions, etc. and at each point in the proof see clearly what these mean. In programming we have variables, arrays, structures, IF statements, loops, subroutines, and without documentation or careful reading don't see clearly what these mean.

Once I tried: I wrote some subroutines for sorting, permutations, etc. and tried to have clear properties for the operations the code die, properties that could reason about. Then for some uses of these subroutines, could do some logical reasoning much like in algebra in math. I didn't go very far with that idea!

Why the hell are you being downvoted? I really appreciated this line of thinking.

Because he argues under the same incorrect assumption that writing mathematical proofs is more fault-proof than writing code. Which is what the answers on stackexchange are partly about.

i think he's arguing that it gives us a more precise language to describe our documentation than just regular comments, not that mathematical proofs are fault proof

I liked this part of one answer especially

> Still, I hope that this sheds some light on the question that is implied: "What really is the difference between proving some theorem and writing a program?" (To which a careless observer of the Curry-Howard correspondence might say: "Nothing at all!")

> I've never heard of someone who wrote a big computer program with no mistakes in it in one go, and had full confidence that it would be bugless.

I've actually done this a number of times before, but only in the ACM ICPC programming contest, so maybe a difference here is the environment in which people write programs vs proofs. In the contest, you have a team of three people and only one computer, and if you submit an incorrect solution, the only response you get back is "Wrong answer" with no detail about what test case was wrong. The typical way that teams approach this is to write code out completely on paper, then transcribe it from paper to the computer, run the provided test cases, and submit. Computer time is valuable, so if you run into a mistake that you can't figure out, it's common to print your code and look through the code on paper rather than trying to debug it on the computer.

When you train enough in an environment like that, you learn to be very careful about all of the details of the program you're writing. A single mistake can dramatically increase the time it takes to solve a problem, and there's pretty much no opportunity to "try it and see" like there is in normal programming. Also, the simple act of writing code down on paper and then copying it into the computer (double-checking as you go) gives you much more time to notice mistakes.

Mistakes are still common, of course, but I've had a number of times where I write out a program on paper, type it into the computer, compile it with no errors, run the sample test cases and have them all pass, and then submit it and and see that it's correct. I've never experienced something like that in any other programming environment, including other programming contests, which typically let you write your code on the computer.

Proofs tend to be the same type of environment: you write it out, with no compiler to help you, and you have plenty of time to read through it over and over before you have someone else check it for correctness. Maybe that sort of environment forces a level of care that you don't see as much in programming.

The answer is simple.

In Mathematics you operate on a much higher level of concepts, and these concepts don't just fall out of thin air, but were sometimes decades or centuries in the making.

In programming though your concepts are made up very much on the fly (if you bother developing concepts at all; usually you just use your framework of choice and hope it got enough concepts baked in so you can survive), and therefore often not very good and coherent. That means you can not rely on them for any kind of correctness assessment.

It's not just that, people spend way more time going through mathematical proofs, finding, and formulating them. If you give programmers time to muse about every function for weeks and write no more than 50-100 pages of program text per year or even less, then their programs will be almost bug free. You get what you pay for.

Note: I'm not claiming that programmers should be treated like mathematicians or vice versa, I'm merely pointing out the differences of the activities.

Edit: There is of course also a more trivial reason. On average, research mathematicians are probably more intelligent, skillful and diligent than typical programmers.

As I said, concepts don't fall out of thin air, it takes time to come up with the right ones. This is the major part of doing mathematics, once you got the right concepts nailed down, the proofs fall out basically automatically.

Programmers are less intelligent, skillful and diligent on average than research mathematicians? How do you figure that? This statement appears to rely on a circular definition of intelligence - maths is "hard" therefore people who do it must be "intelligent".

Given the examples in the linked discussion of cases where not only did mathematicians write buggy proofs but it took years to figure out a mistake existed at all, let alone what it was, I find it hard to believe that. To the extent it may appear superficially to be true it's likely the result of the academic setting in which there is no connection to real world relevance and the only pressure that exists to get things done comes from peers and the need to publish papers - but if those papers achieve very little and your peers papers also achieve little, that's totally OK.

Compare to the world of the working programmer who is judged not by how fast he writes code but by the real world positive impact of that code, and it is easy to see how the mathematician may come across as more diligent or intelligent. But it's just an artifact of the pressure-free environment.

I was also surprised to learn that the idea of checking mathematical proofs using Coq is considered just as exotic or impractical as checking programs. I had thought that Coq and other proof assistants were in wide usage for this use case, as surely pure mathematics is simpler to reason about formally than entire programs ... but apparently not. The fact that maths proofs are still mostly checked by hand, whereas machine-checked proofs (like static type systems) are widely used by even novice programmers, is hardly reassuring.

Research mathematicians are certainly more highly trained than non-research programmers, at least for the first few years of their career. A PhD, at least in the USA, is really intensive.

What’s the connection between being highly trained and being “intelligent, skillful and diligent”? Circus animals are definitely highly trained after all.

All math PhDs can become programmers.

Some might be too bored to be good programmers, and some might have issues with corporate nonsense and workplace politics. But purely in terms of the ability to manipulate symbolic systems to useful effect, the base level is more than high enough for most programming jobs.

Evidence: for a long time, math BSc/PhD quals were highly valued by software houses. This continues to be true to an extent, especially at the high end with FP/ML.

The percentage of programmers who can become math PhDs is... lower.

> All math PhDs can become programmers.

First of all what does "can become" mean? If it means with sufficient training and supervision they can learn to be programmers, then that's also true for the inverse.

Furthermore, we need only one counterexample to make it false, and I happen to know a few math PhDs that are not that great at programming even though one of them actually works as a programmer.

> If it means with sufficient training and supervision they can learn to be programmers, then that's also true for the inverse.

No way. Most programmers are genetically unfit to do research mathematics. Many programmers can't take in an idea and expel it back out without corruption because they've got some cosmic ray simulation device in their brain stem. Or they just don't have the creativity. For example, think of all the people that complain about interview warm-up questions or think they're something you'd memorize.

This largely ignores the fact that research is 90% reading papers (or doing lab work in less pure fields) and trying to come up with something. Fighting for money, writing papers, producing graphs/charts, etc.

Pure maths research is undeniably simpler, but not that much. Look at HoTT (homotopy type theory), or reverse maths (https://github.com/ericastor/rmzoo/). These are sufficiently close to programming - because they are largely composed of programming tasks.

Furthermore, researchers usually don't do work alone, they are usually enrolled in some kind of a program, with a supervisor, mentor, guide, or at least a program/faculty chair. And even if they are totally on their own, they can start doing work on unsolved problems. Usually people new to research start by doing a survey paper for a certain field, to get an overview of recent and past progress and problems, solutions and techniques.

Oh, and this also applies: https://78.media.tumblr.com/41b40230404ccfd7af8a0146ea6689d3...

Yes, 99.9% of programmers would never become the next Tao, cranking out blog posts, books, polymath papers, lectures and otherwise results every few days/months, but that doesn't mean they couldn't do pure maths research. But luckily they don't have to. Because it's a very different realm than programming. (Or even protocol design, IETF work, low level microcode work, or run of the mill mobile apps.)

Some contemporary mathematical theories such as "Inter-universal Teichmüller theory"[1] are so complicated that only one or two dozen people in the world can understand them. Proof assistants like Coq do not help with those kind of theories at all. In a nutshell, research mathematics has become fairly complicated, to say the least. (I'm saying that as a layman, from what I've gathered about it. I'm not a mathematician.)

> Programmers are less intelligent, skillful and diligent on average than research mathematicians? How do you figure that?

Well, the selection process is much harder. It's an empirical claim that could be falsified, but the claim seems reasonable in lack of any counter-evidence.

[1] https://en.wikipedia.org/wiki/Inter-universal_Teichm%C3%BCll...

> only one or two dozen people in the world can understand them

It's more that only a few have bothered to.

> This statement appears to rely on a circular definition of intelligence

The statement is a metaphor. Mathematicians are commonly deemed intelligent, with high variability of course, as university graduates generally are. On the meta level, mathematicians provided a lot of the basis which computers and programs are build from. Now it's poetic freedom to include programmers who venture into mathematics in this fuzzy term.

"Programmers are less intelligent, skillful and diligent on average than research mathematicians?"

Keep in mind that there are a lot more programmers than professional mathematicians, and programmers are more likely to be well paid than mathematicians. As a result, mathematicians are self-selected for doing math while most programmers are only in it for the paycheck, on top of the fact that a mediocre mathematician probably isn't going to be able to make a living in math.

"Compare to the world of the working programmer who is judged not by how fast he writes code but by the real world positive impact of that code,..."

I suspect that you have an excessively positive opinion of the work of most programmers. I myself know far too many who are both slow and detrimental to the projects they are assigned.

As for formal mathematical proofs, I bet you will find that most mathematicians don't do them for the same reason that essentially no coffee is verified: it adds a lot of complexity (the same complexity, I suspect) without any obvious benefit.

I think it's largely a product of resources. There are fewer positions and more people who want to become research mathematicians so only those who are extremely well qualified even get to the post. The reason for the lack of resources is that the research mathematician's work isn't usually immediately profitable (hence their pay is often relatively low relative to their software engineering counterpart). By contrast, many companies operate their software development process in a way that allows them to recruit developers with minimal training and even deploy them in a way which they find useful, even if in fact that work might be completed more quickly by a smaller group of more experienced/capable programmers.

I think you're right about the pressure-free environment bit, too - some places developers are so bogged down with fire-fighting that planned development with real foresight rarely gets developed.

Moreover I think there are just more software developers, with much more variance in their abilities than research mathematicians.

I think it's not an apples to apples comparison.

In mathematics, there are abstract concepts like integers. For any i, i+1 is also an integer.

In programming, there is a MIN_INT and MAX_INT. If you write i/2, it's different than i/2.0. If you store a long string in a database, the column may be cut off at 32 chars because of the column type. Running string algorithms that sounds perfectly reasonable on ASCII may result in weird outcomes on Unicode. Most of these things also depend on the programming language, the compiler (MS, gnu, etc), the compiler version, OS, libraries, sometimes even the locale! A provably good crypto algorithm may be vulnerable to side-channel attacks. A mathematician may be happy to give an existential proof, but a programmer needs an implementation, and one that is polynomial [usually]. And so on...

The tldr is, the real world is more complicated, limited and nuanced than the abstract concepts of mathematics.

Compare writing a proof in Coq to writing a normal program. That is far more equal in terms of what you're doing. Writing a proof for people implicitly assumes a mountain of background information and interpolation between statements that doesn't exist in programming.

As the top voted answer says, proofs are at a very high level compared to programming.

Now imagine writing proofs on a very low level (check Metamath) where you work with wff and rewrite rules. It gets as tricky as programming.

I feel less confident of my proofs than my programs, because I can't run them, to see what happens. Yes, there are proof assistents like coq, but mathematicians look down on them.

Proofs are usually about some very small thing, and require a tremendous amount of work. Then, there is a huge literature for guidance and reusable elements (though, a lot of work to use it), and peer review to check it (also labour intensive).

I do not understand why mathematicians look down on proof assistants. I've heard this claim multiple times and it continues to make no sense to me.

Are there any mathematicians here who can weigh in?

Not really a mathematician, so take this with a grain of salt. I would guess there are probably several different reasons for "looking down" on proof assistants.

On the one hand we have something like the 4-colour theorem where there is some kind of "proof", which is very large and incomprehensible. This is probably unsatisfactory to many because one is not really interested in just knowing that something is true, but ideally one also want an understanding of "why" something is true. This is, to various degrees, achived in more standard proofs.

Another reason for disliking proof assistants is probably that they simply are very cumbersome to use and not very much can be proven with them so far. I would guess that even if you could get someone to admitt that the idea is cool and could be very useful, it's just not practical and for most people in mathematics it's just a distraction from what they are trying to work on at the moment.

Compare with trying to convince someone that a flying car is really cool, yeah, sure, it probably would be, but so far it's basically sci-fi. If you want to work on building this, great, but most commuters will probably "look down" on your idea if you start bugging them about it.

It is a bit similar to why we don't use program verification tools very much in software development. They are very complicated to use and while they do a good job at verifying existing code they don't help as much when writing code from scratch, because they tend to add extra obstacles at this stage.

From what I have seen, proof assistants in math are used when extreme rigour is desired (which is not always the case) and when working with extremely long computational proofs with hundreds of cases (where you need to work at a higher abstraction level; a human writes a program that outputs the proof and then the proof checker verifies that this extremely long step by step proof is valid)

Mathematician here: It isn't exactly that proof assistants are looked down upon. Rather, most of us don't do 1st order logic and it isn't on anybodies radar. Even if it were, it is often new proof techniques that lead to new interpretations, generalizations and discoveries about what we should be trying to prove in the first place. It is very hard to interpret a wall of 1st order logic.

Not to mention decidability issues.

Both Isabelle and Coq are based on higher-order logics, so I am not sure how first-order logic is a barrier to entry. Especially Isabelle is very easy to use because the logic is so standard with nothing really surprising or especially restricting (a very strong form of the axiom of choice is deeply embedded in the system, so it's probably harder if you care about it at this level).

Regarding your second point, to me this looks pretty much the same as in software: In high-quality code I expect high-level comments that give me intuition about the code, and I also expect high-level documentation giving me further intuition about the components and the system as a whole. The more complicated the system is, the more important the comments and the documentation become.

I see no reason why we should hold computer-assisted proofs to a lesser standard.

I am not a professional mathematician but I worked with proof assistants semi-professionally. The problem is that proof assistants doesn't cover everything that is required by mathematicians, proofs are often verbose, and unreadable.

There's some attempts to alleviate these problems, which are named Homotopy Type Theory, and they are quite successful.

Anybody interested, this 2016 paper is a general survey of the current proof logic refinement implementations out there, and the problems and limitations they have which they are currently trying to solve with dependent types/Computational Higher Type Theory http://www.redprl.org/pdfs/afpr.pdf

It's because a good proof conveys human-level insight first and foremost, and the details are often mental baggage that can be sorted out later.

Proof assistants are the opposite. Sacrifice intuition and insight for the sake of correctness.

This is also why mathematicians love picture proofs.

I am not satisfied by picture proofs, I'd like to see derivations from axioms and known results.

I love pictures that give me intuition about a proof and I agree that intuition is crucial to understanding. But all the intuition in the world is useless if the proof fails because of one tiny logically unsound step or one pathological corner case, so it's no good to ignore the technical details or, even worse, to become unable to expand a purpoted proof one has written into a fully detailed version, which I suppose can easily happen if someone relies too much on intuition.

Of course you can't ignore details. I was explaining the source of emotions, which tend to drive whether one wants to adopt a particular tool or method.

That being said, I often find convincing, false proofs as illuminating as true proofs, once the flaw is clear, because they highlight the nature of the conjecture. So I disagree with your claim that a proof can suddenly become useless due to a slight misstep.

And for what it's worth, theorems are rarely thrown out due to pathological corner cases; at least I've never heard of this happening. Instead, if the insight conveyed by the proof is useful, it's called a partial result and the conditions are modified to fit the proof. Entire theories are built up specifically to avoid pathology (almost every mathematical field does this)

I'm a professional mathematician and, candidly, most people in my subfield don't really know that they exist. I do, and would love to use them, but I find them very difficult to use and don't have good examples of proofs relevant to my work.

To be specific, I've used Coq in the past to help verify properties of programs such as a sorted list really being sorted. That said, I primarily work in applied math areas such as optimization, numerical linear algebra, and numerical PDEs and I have no idea where to begin with fundamental proofs such as Newton's method converging quadratically within a certain neighborhood of the solution. Alternatively, I'd love to see formalized proofs of the theorems that we'd learn in a course in real analysis such as one based on Rudin's Principles of Mathematical Analysis. Really, if anyone has examples of these, please let me know.

There's an amazing number of errors in published work. Most of the time, the work is still mostly right, but that's not OK. In my opinion, we'd be better off with formalized proofs.

> I primarily work in applied math areas such as optimization

It may be rather an off-topic, but I suggest you to read my funny paper: https://docs.google.com/document/d/10pTRJFgwEGnUM5RF1CHX2OO5...

I had experience both of writing programs and writing proofs including proofs in formally verified languages, e.g. Coq, Agda.

First of all, I think that the author underestimates the complexity of writing correct programs. What if integer overflow occurs? What is some exceptions happens somewhere? Programmers rarely consider all the pathological cases, while mathematicians must consider all of them. If program works most of the time, it's good enough for programmer but not good enough for mathematician.

Second, thanks to Curry Howard Correspondence, every formal proof has a corresponding program which 'constructs' a result of the theorem from preconditions, so, the proof is basically a program (and vice versa in a typed programming language).

In mathematical theorems the initial conditions are rather uniform without much if any of special cases. Thus mathematical proofs needs typically much less control flow to cover the initial conditions than computer programs. In fact many proofs are just straight deduction without single if to cover corner cases. Such type of "code" is simple to check. One just checks for logic of deduction, not the coverage of all initial conditions.

Adding to the arguments present here already, it's also often easier to work with mathematical formulas and concepts compared to programming concepts. For example:

pi. Easy in "math", effing hard to do in code. You don't have to worry about iee floats in "math". You don't have to worry about computational restrictions like ram, cpu time, null pointers etc.

Because in a program you can't have functions having their implementation left as an exercise for the computer. :^)

Both theorem proving and programming operate on an abstracted view of reallity ( in case of mathematics this reallity is often determined by some choice of axioms). By some metric the abstracted reallity of programming tends to be more complicated and noisy than that of mathematics.

One extra element I'd add is that what counts as an error in a proof is different than what counts as a bug. In pure math, an error is a strict failure of logic that breaks the proof. In programming, a bug doesn't need to only refer to something that stops the code from working. I've also heard it referred to as something that stops the code from working properly or efficiently, for instance. Mathematicians don't care about that because they have a different goal than a programmer, that is, to prove the truth of something (though some are motivated to produce more "elegant" proofs).

I don't agree that mathematical proofs are more fault-proof than code.

Mathematics is based more in the "spirit" of the idea and proof, rather than pedantically driving things down into the ultimate nuts and bolts. Many paper proofs are likely full of bugs deep in the details.

As intuitionism and machine formalism develop, and the standard of rigor rises, we might see entire branches of mathematics being relegated to the dustbin of historically interesting human endeavors but totally useless as foundations/formal assumptions for future work.

Two words, iteration and conditional execution.

Most math lacks these features common in programming.

With iteration you blend the results at time t with the results at time t+1.

Because of conditionals (if statements), a programming mistake at time t may not become evident till some much later step in the iteration, because the path through the logic is not guaranteed to be consistent.

Typically the data of all intervening steps has been lost by the time you encounter the error.

It was posted dec 11 2017, not dec 2011 :)

Most programming languages are unsound logic systems which allow us to prove true==false rather too easily!

If I spent as much time on a few lines of code as I spent in high school on a few lines of a proof, they'd be just as bug-proof.

Nobody is going to pay me to spend that kind of time on that little amount of code. Heck, I'm not even going to spend that kind of time on my own projects.

Because one is dealing with abstract theory with specific rules vs engineering in the real world.

One exists in the world of abstraction while the other lives in the real world.

Might as well ask why we can have a perfect circle in math while a perfect circle doesn't exist in the real world.

Because the interpreter for mathematical proofs is far more forgiving than the interpreter for code.

x = x + 1

I remember the fist time I saw that line and said, that's false. And it's been an ever ending divergence from pure math for the past 30 years.

It can also be:

x <- x + 1

x := x + 1

But I guess since assignment is more frequent than equality checks, most PL designers opt for using equals. I do like R's left arrow assignment operator. If only keyboards had a default arrow character key. It would completely get rid of a class of errors based on forgetting the second equals sign.

A sane compiler always give a warning when doing a comparison outside a condition and when doing an assignment within a condition.

Not sure if really related but I couldn't follow the math at school. For example in algebra the rules were complicated and required you to know things that are not explicitly set. Because of that I wrote my own functions to do what my teacher said. Then in the exams we are allowed to bring formulas, therefore I bring my own JavaScript function and I was the compiler :)

The teacher steps would resume in 5 sentences, but the function would be more long and include exceptions and weird cases. No room for mistakes with my JavaScript. No wonder I had the biggest score in the classroom.

What level algebra and school are you talking about? I don't really see how any teacher would allow this. Mind explaining more?

University.

I think the resounding answer has been over the years that written proofs aren't more fault proof, they're just better at hiding the faults because they lack explicitness. There has been a recent push for formal verification because it's easier to actually find issues with the proof.

Just peruse any upper level undergraduate math text. Flip to any proof and you’ll find “it follows naturally that...”

The bane of my existence as a math undergrad.

These days programming languages actually are used for expressing proofs. They can automatically check them to. For example the Coq theorem proving language.

https://en.wikipedia.org/wiki/Coq

Some would argue that writing code IS more fault proof than writing proofs the traditional way.

I would still trust a mathematical argument I can understand over the output of some automated theorem prover.

Of course these aren't mutually exclusive, provided the theorem prover is simple enough to understand.

Because it's not true :-)

Writing mathematical proofs is as fault-proof as writing pseudo-code.

Writing machine-check proofs is as fault-proof as writing code.

I like the Lamport answer, implying that proofs are just as faulty as programs, they just don't get tested https://cs.stackexchange.com/a/85362/23759

One might say the amazing thing is that many (not all!) such theorems are correct, despite the errors. Somehow, mathematical insight sees the truth, despite formalism failure...

But, by this standard, most programs are "correct", they just have some inconsequential errors.

I think this goes to a systemic problem in mathematics, that proofs are not very rigorous. I've never found one convincing. Instead, math is slightly like English Literature, where you learn "theories" that are held to be true by the community. You get inducted, and off you go. It's not purely objective.

Of course, this doesn't explain the usefulness of mathematics when applied to reality, so I only claim it's "slightly like" an Arts subject. Perhaps some survivor bias, and engineers fix any problems.

> I think this goes to a systemic problem in mathematics, that proofs are not very rigorous. I've never found one convincing. Instead, math is slightly like English Literature, where you learn "theories" that are held to be true by the community. You get inducted, and off you go. It's not purely objective.

This is an outrageous exaggeration.

Because we generally only accept mathematical proofs from highly-trained experts, and no one would hire the kid next door, who taught himself math and seems to spend a lot of time fooling around with calculators to do professional work in mathematics?

Depends on how you define fault here. Is it mere logical correctness of code or any error that might occur when code executes. If we follow former definition of fault then , they both are similar in being "fault-proof". If we follow later definition then execution environment of the program comes into play and it depends on a lot of variables and their complex interplay, that it becomes much harder to provide any formal guarantees of fault tolerance.

However there are execution environments, read RTOS that try to be fault tolerant. Also various virtual machines like JVM,CLR try to provide fault tolerance to varying degrees.

With maths, you're merely discovering something which already exists. Programming is more like you're creating something new.

You know all the preconditions and constraints ahead of time.

With real world applied software that is very rarely the case.

math resides in the land of abtractions(fantasy land) and actual code has to run on actual physical machines in the real world. In the real world you can't just state an axiom and fix bugs as math people have solved all their problems in the past 150 years.

What? If this is true then there are a whole lot of misguided mathematicians out there working on "solved" problems. If they could just add whatever axiom seemed useful math research would be meaningless.

If you're saying that math/theoretical computer science makes unrealistic assumptions, that's a different (and more reasonable) claim.

That is not what I said. What I said is that math ultimately doesn't need to and doesn't want to deal with reality. The "proofs" they create do not even have to be consistent with each other, you can pick whatever you need...

Posted 11 Dec, 2017, not 2011.

Very few real time interrupts in math proofs.

[Meta] Why do people respond in the HN comments with answers to this question? Do people not realise that this is a post to a thread, wherein the value (and the answers) are in the original link, on stackexchange?

Not really because the StackExchange thought police really does not let people freely answer the questions. It means in practice that if you write an answer not in alignment with the correct thought you get scolded and penalized.

What? Answers there disagree all the time.

You have an example of this kind of thought police behavior? In all my years on that site I have never seen anything like what you are describing.

I’ve experienced it often. I came across a question pertinent to a problem I was experiencing, I tried the work-around in the comments, it didn’t work, I mentioned this and was moderated to oblivion and attacked; I created a new issue, and drew fire for then answering it myself (but also accidentally using a comment to do so); I got hollered at for creating a link between the two issues; I was downvoted for being new. It’s a totally hostile environment. As of then I consider it a Read-Only resource (plus my questions never get answered anyway).

I'm sort of amazed that I find anything of value on there, given the same experiences.

The structure of Stack Overflow is designed to get question and answer pairs that contain the critical information and are easily discoverable by google.

Questions and answers that have value and that follow that model are likely to be more discovered by people using Google.

There are many people who consider all social media sites to be "the same" - basically posting whatever they want. Be it forums and facebook or whatever random idea hits your mind on Quora. Those are different models and work for different types of problems. An asynchronous debugging session likely works better on a more forum like site than Stack Overflow... and yet people post such questions to Stack Overflow. When those questions are found, the people who are entrusted with the various community moderation privileges, in an attempt to follow those ideas of "This site is all about getting answers. It's not a discussion forum. There's no chit-chat." (from the tour) will use those moderation tools to try to make the good stuff more findable and the stuff that makes the good stuff harder to find... well... gone.

There are many different sites out there that have different focuses. Stack Overflow (and the model the rest of the Stack Exchange sites use) is trying for one narrow slice that they can do well. People that want a forum should look to a forum... those who want to ask for opinions and anecdotes should look to sites that do that better. Stack Overflow is not intended or designed to be the be all and end all of software questions.

Thanks for the reply, but this doesn't explain why correcting answers is so frowned-upon. Or a general hostility in tone from the mods.

No worries. I find that in practice the kinds of questions that I can't answer for myself (the kinds for which a natural language question rather than a straight Google search for documentation is helpful) are almost always already answered anyway. So having it a read-only site is not a big deal.

I think their model does indeed turn away a lot of people with good experience and intentions, and even leaves a lot of incorrect cruft lying around, but overall it's a mostly-beneficial source of information, with, as you say, high searchability.

First note - "mods" - only the people who have a diamond after their name are mods - https://stackoverflow.com/users?tab=moderators - its a rather small group.

Everyone on the site who has 15 reputation or more can participate in community moderation to some degree or another. There are people within that community who use the community moderation tools of voting frequently in an effort to have the site match their vision of what it should be... but they aren't mods.

When dealing with thousands of questions per day (90% of which are crap https://en.wikipedia.org/wiki/Sturgeon%27s_law ), the amount of time they have to work with any one post is very limited. Often people are terse in their comments - it takes time to sit down and write a thought out reply... and that is very limited in comments if it isn't an answer itself (and to that point, that is by design).

This terseness of communication is often interpreted as rude. Its not intended to be - its just the medium and limitations. Yes, sometimes people are rude. The thing to do in these cases is flag the comment as rude - if there is a pattern with the behavior, the moderators (with a diamond) handle the flag and will take it up with the user who is rude. Saying that your code does not work as described in the question, however, isn't rude.

I applaud your use of google first. There are so many people who fail to realize that the goal of Stack Overflow is exactly for people like you - who search with google and find an answer and never need to ask a question on the site themselves.

The significant amount of incorrect cruft laying around is a side effect of people not using the moderation tools (downvotes on questions can make the questions get deleted and make search results better) or a value proposition that has entered the collective community moderation of "anything that attempts to answer the question has value and shouldn't be deleted." Unfortunately, that later point reduces the value proposition of the site and diminishes its utility.

> drew fire for then answering it myself

Which is really weird and unfortuante. Asking and answering a question yourself contributes useful information to the site.

Answering your own questions is also explicitly allowed -- you are informed as such on the page where you ask questions.

By the sound of it, I suspect expect that what the parent drew fire for was answering his own question using a comment.

I answered myself with a comment, which was a faux ps. It’s rectified now.

There are many Stack sites. Stack Overflow with its 6k questions/day has (by necessity) a different moderation approach than Computer Science.SE that has 16 questions/day.

That difference of several orders of magnitude in incoming questions results in very different moderation approaches. You can spend 15 minutes reading every new question and answer every day compared to trying to filter the 90% of crap that gets posted on SO in a few seconds. This means that new users can be given more guidance in crafting a question and getting answers... though again that depends on a user putting the time and effort into writing the question and making sure they understand the scope of the site first.

Each site has a different set of users who are using the moderation tools to make the site into the one they want to see. The highest rep user on CS.SE has substantial rep on CS, Math, Theoretical CS, MathOverflow, and TeX (not Stack Overflow). The next highest has rep on CS, Information Security, Cryptography and Theoretical CS (again, not Stack Overflow). The next highest is CS, Theoretical CS, TeX and then 2.7k (not even enough for a close vote) on SO. Followed by a user who has CS, Academia, Aviation, Travel, and English Language Learners (not SO). This is a different community with different goals - in particular, this one is about the mathematical underpinnings of computer science... and that shows in its user base.

The different sites have different personalities as well. The main SO can be brutal just because the herd responses can be so swift. Niche categories tend to be friendlier, Aviation.SE for example. Gaming, Movies, and Sci-Fi all seem really friendly for the fairly large volume they see.

I have heard that chicken farmers have to monitor young chicks carefully for injuries that produce bleeding because when the other chicks spot one, they will relentlessly peck, which is likely to quickly kill the bleeder. Regardless of whether this is true, it’s a decent model for how drawing a bad initial response to a question can be fatal as the other chicks pile on. I once made the mistake of asking on Workplace.SE whether the HR profession had empirical support — as opposed to the usual conflicting folk wisdom — for whether including personal interests on a resume is helpful[0]. An early answer clearly failed to comprehend the question at a basic level, but it nonetheless was the initial spot of blood. Comments from multiple moderators saying the question was reasonable were not enough to stave off the pecking.

[0]: https://workplace.meta.stackexchange.com/questions/4888/ques...

Aviation gets 9.2 questions/day. Arqade gets 23. Movies gets 16. SciFi gets 31. Combined that is 80 questions/day. About 1/4th of what the Java tag on Stack Overflow has gotten today.

You've got a higher percent of users who are more willing to invest the time necessary to help new users and a larger body of "good questions" that serve as examples.

Niche categories tend to be friendlier because you will see the same people more often and and have interactions with them more frequently. The vast majority of users on Stack Overflow ask a question (toss a bunch of text in a text area) and disappear. Pulling up the front page, you get questions where the entirety of the body of the question is:

> "i need to scan part of page by ImageEn in delphi for faster scanning like window7 paint scanner dialog! (screenshot)" ( https://stackoverflow.com/q/48050760 )

and

> "Hi I have the promblam the I want to sent with volley post a string to my php script on a server and get a Jsonarray. But I search a long time but didnt get an answer. Can sombody help me with that." ( https://stackoverflow.com/q/48050744 )

And remember that every minute there are 10 new questions asking for help in a similar fashion. When there are 10 questions a day, people can spend 1/10th of the time they're going to spend on moderation on the site commenting, editing, and helping every question. Lets say that's 6 minutes. Where there are 6k questions/day, or several hundred in the preferred language tag/day - you (and other people) making judgement calls on the order of seconds. Down vote and move to the next? Comment about how to improve?

It is very difficult to spend sufficient time to get people to update their question for it to be helpful. When I participated, I was hesitant to spend any more time doing community moderation than was evidenced by the person drafting the question. If they spent 10 seconds writing it, I'll spend 5 seconds reading it and 5 seconds voting on it. If they spent 10 minutes writing it, crafting a MVCE and getting the punctuation and grammar correct... I'll spend 10 minutes working with them trying to get it into the best question it could be. But if I'm only going to spend an hour... that's 1/6th of my time budget. It works when there's only a dozen questions/day but fails miserably when there are a few hundred.

https://meta.stackoverflow.com/questions/251758/why-is-stack...

I'm quote familiar with that post, the linked questions and comments are often quite interesting to read as a bit of social commentary. On large communities decaying over time, being nice or mean, and Stack Overflow ( https://meta.stackoverflow.com/questions/256003/ ) is another read that I would suggest about the social dynamics there.

Much of this has to do with a conflict between two visions of what Stack Overflow should be. Elsewhere (private slack channel post), I've mused about those visions:

++ The Atwoodians

Those who are drawn to the site by the original call for the site ( https://blog.codinghorror.com/introducing-stackoverflow-com/ )

> It is by programmers, for programmers, with the ultimate intent of collectively increasing the sum total of good programming knowledge in the world. No matter what programming language you use, or what operating system you call home. Better programming is our goal.

There is a word in italics there - its in the original. It is about good programing knowlege. Not all programming knowlege. It is about high standards and quality. This presents a higher barrier to entry and some degree of eliteism. It is also a vision of what the site can be.

Close and delete questions that aren't good. Delete answers that aren't good - especially if they make it harder to find information.

++ The Spolskyians

The Spolsky vision differed a bit, and it is hinted at in Joel's launch anoucement. ( https://www.joelonsoftware.com/2008/09/15/stack-overflow-lau... )

> In addition to voting on answers, you can vote on questions. Vote up a question if you think it’s interesting, if you’d like to know the answer, or if you think it’s important.

> ...

> What kind of questions are appropriate? Well, thanks to the tagging system, we can be rather broad with that. As long as questions are appropriately tagged, I think it’s okay to be off topic as long as what you’re asking about is of interest to people who make software. But it does have to be a question. Stack Overflow isn’t a good place for imponderables, or public service announcements, or vague complaints, or storytelling.

Things that are interesting and helpful to someone. The annoucement encourages polls and questions with dozens of answers (the example being favorite keyboard shortchut in emacs). This is a different vision than the Atwoodians subscribe to and there are occasional debates to be seen on meta between people with these different visions.

Hot network questions that bring in more things that are interesting are wonderful. And they upvote interesting things to make it easier to find them too. In general, deleting posts should be avoided because it might be interesting or helpful to someone.

----

These two visions of what the site should be play out, and new users who aren't aware of the background can get confused as one post or another attracts the attention.

There are also people who come to the site with a view that its like facebook and since people like getting a :+1: on facebook, they should get it on Stack Overflow regardless of the material - it makes them happy and its good for people to be happy.

There are people who are using Stack Overflow as a differentiator between their resume and the hundreds of other applicants. Any down vote on their questions or answers impact is seen as impacting their future career prospects.

And then there are the people trying to keep their "develop a clone of facebook" bid that they made on eLance to under $100 costs that they're writing between classes on on the weekend so they have some left over for beer money.

If you're also qubex on SO [1], then I'm not seeing any of that hostility. Did it get deleted, or is it that my perception differs because I'm an unrelated third party?

[1] https://stackoverflow.com/users/3637244/qubex

Yes that’s me, and yes there’s been a significant amount of a posteriori revisionism.

As somebody else pointed out, I answered my own question with a comment, which seemed innocuous enough, but was actually a formal faux pas. I guess I had it coming, I didn’t want to make myself out to be innocent and aggrieved, but it struck me as a bit harsh. Then again, everybody always feels they have been treated too harshly...

An issue with Stack Overflow is that the site incentivizes people with badges to review and disposition large numbers of questions and posts, which spurs Fastest Gun in the West competitions. For a new user unfamiliar with the culture, this can result in a question being downvoted and closed within minutes — not a terribly welcoming feel.

Changing the site’s incentives to reward soft skills such as mentoring and encouraging new users seems like a really hard problem.

Answering your own question is 100% in bounds; no one should criticize you for that. However, an answer should be posted as an answer, not a comment. My imagination fails early in the morning pondering how one might accidentally use a comment for an answer.

In the original question, was the workaround a comment or an answer? Did you stop at “didn’t work” in the failure report?

Got a link?

StackOverflow, and Wikipedia even more so, are real life Stanford prison experiments on the inside. Power, in whatever form, seems to attract abuse and catalyze a bit of megalomania in the holder.

You do realize that Standford prison experiments had such a flawed methododology that they are not considered scientificly accurate anymore?

For one, they did not do sufficient backgroud checks on intake, so the volunteers were self-selected group of people with sadistic tendencies.

Also, researchers were not fully neutral, they were (conciously or not) encouraging subjects to violent behaviours, thus steering the whole study towards expected results

Since wikipedia and stack overflow allow for self-selection, and encourage heavy use of editing power, the stanford prison experiment seems like a great analogy for them, but it is nice to hear that the experiment may not represent the tendencies of an average human given power.

>You do realize that Standford prison experiments had such a flawed methododology that they are not considered scientificly accurate anymore?

You do realize that that's not relevant to what the parent said?

Which (whether correct or not) boils down to that *Exchange sites attract authoritative moderators and gluttons for abuse and punishment users, akin to the Stanford prison experiments.

It's just like here on HN where you MUST agree with the crowd or else your comment will be disappeared.

IMO, we need better commenting systems in general.

Last year I read HN many times a day and often staying awake two days in a row, I've observed that phenomenon you're describing. And from what I've observed, that crowd is different (and stonger) when the Americas are awake than when Europe is awake.

There seemed to be less downvoting around 10am GMT than at 6pm GMT.

I think it's just that less voting in general happens when America is asleep. At least that's the conclusion I drew from my unhealthy sleeping habits.

The problem is that content providers have a financial incentive to create an environment that penalizes anything controversial and rewards unchallenging posts that regurgitate whatever the lowest common denominator of that community happens to be. Reddit is by far the worst example of this, but it feels like HN is becoming more like that as time goes by.

Isn't there always everywhere more people interested in a subject than experts and groupthink with wrong and not well informed opinions becomes inevitable? At least on HN you are free to attempt to influence the groupthink.

Good thing there are no thought police on HN.

Because people also want to discuss their OWN answers, with the HN community, do some people not realize that?

Because the proof checker is a smaller piece of software to find bugs in, and used by more people so more people look. Simple.

Reply on news.ycombinator.com