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!
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
> 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!")
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.
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.
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.
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.
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.
> 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.
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"
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?
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.
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
These days programming languages actually are used for expressing proofs. They can automatically check them to. For example the Coq theorem proving language.
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.
[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.
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).
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.
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.
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.
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.
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:
> 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.
> 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 ...
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?
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?
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.
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.
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.
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).
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.
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
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 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.
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".
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.
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.
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.
143 comments
[ 4.7 ms ] story [ 200 ms ] threadNow imagine writing proofs on a very low level (check Metamath) where you work with wff and rewrite rules. It gets as tricky as programming.
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!
> 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!")
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.
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.
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.
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.
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.
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.
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.)
> 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...
It's more that only a few have bothered to.
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.
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 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.
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?
What you're describing is essentially a proven, lightweight, formal method for improving software quality. Many commercial apps use it.
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
QED . []
https://en.wikipedia.org/wiki/Coq
Some would argue that writing code IS more fault proof than writing proofs the traditional way.
Of course these aren't mutually exclusive, provided the theorem prover is simple enough to understand.
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.
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.
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.
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.
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.
Which is really weird and unfortuante. Asking and answering a question yourself contributes useful information to the site.
By the sound of it, I suspect expect that what the parent drew fire for was answering his own question using a comment.
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.
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...
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.
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 ...
[1] https://stackoverflow.com/users/3637244/qubex
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...
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?
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
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.
IMO, we need better commenting systems in general.
There seemed to be less downvoting around 10am GMT than at 6pm GMT.
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).
Are there any mathematicians here who can weigh in?
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.
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)
Not to mention decidability issues.
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.
There's some attempts to alleviate these problems, which are named Homotopy Type Theory, and they are quite successful.
Proof assistants are the opposite. Sacrifice intuition and insight for the sake of correctness.
This is also why mathematicians love picture proofs.
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.
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)
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.
It may be rather an off-topic, but I suggest you to read my funny paper: https://docs.google.com/document/d/10pTRJFgwEGnUM5RF1CHX2OO5...
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.
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.
Can you provide any examples? I know this is true, but I'm interested in examples you have off the top of your head.
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".
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.
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.
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 real world applied software that is very rarely the case.
Writing mathematical proofs is as fault-proof as writing pseudo-code.
Writing machine-check proofs is as fault-proof as writing code.