Can the same individual accomplish more with programming than proofs?

I think a critical point here lies on what exactly you're accomplishing when you're programming. A person could spend a lifetime on improving Google's ad network, make an incredible amount of money from it, and for all that have not accomplished very much in the sense that we care about accomplishment.

One question that comes to mind is "What would happen if everyone did this?". To me, it seems straightforward that we don't want everyone writing proofs to switch over entirely to programming, nor do we want everyone coding to switch over entirely to writing proofs. We would want a certain proportion of people doing proofs, and other proportion doing programming. Each person's own experiences and talents would determine which one is more useful, but on-balance we might have some proportion p doing proofs, and 1-p doing programming.

So, the question of "Can the same individual accomplish more with programming than proofs" turns into 2 questions - the situation that person is in, and also the global context of whether society is doing a good job at maintaining p provers and 1-p programmers for the overall benefit of society.

For my money, I think society has made p too small. There are way too many good reasons to go into software engineering as opposed to math and CS (namely $$$$) and as a result the social benefit of proofs is under-explored. I don't think however, that I would accept very bad odds for that bet like 1:100 or 1:1000. Proofs (and the societal structure, academia, that has been created to create proofs) have their own problems and as such it's very hard to even determine what p should be.

The Curry-Howard correspondence would like a word. Any time you write a program, you are also writing a proof.

Mechanized proof checkers leverage this idea to enable users to specify formal proofs as programs.

What if you proof the correctness of a compiler? Do you then transiently get all the achievements of all safety critical software that was then programmed with it?

The value of the proof comes from the things it enables. I guess the Rust memory safety guarantees are based on some proofs?

You might find some more thinking about this in the field of Computational Science and Engineering (aka CSE). This is related to computer science, but distinct (often a separate department).

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

Some universities call these "Scientific Computing" as well. E.g., https://gradadm.seas.upenn.edu/masters/scientific-computing/

There is even an industry journal (closely linked to high performance computing). Of course this CSE is said to mean "Computing in Science and Engineering" (just to add confusion):

https://www.computer.org/csdl/magazine/cs/2022/01

Here's a paper that touches on some of the challenges of implementing proofs (and other scientific theory) in software. https://f1000research.com/articles/9-1192

There are about 30 million coders in the world [1]

And about 80 thousand mathematicians [2]

So about 375 individuals programming for every 1 person writing proofs

If we assume this configuration is optimal, then my answer to your question is that if you had a group of 10000 people who like programming and proofs and have 9983 program and 27 write proofs this would be the best way to “accomplish more in life”

[1] https://www.future-processing.com/blog/how-many-developers-a...

[2] https://mathoverflow.net/questions/5485/how-many-mathematici...

Depends what you mean by “more.”

You can write programs to search for and do other things with prime numbers. However this can only tell you about specific prime numbers.

With proof you can prove things about all prime numbers or the integers as a whole. For instance Euclid proved that there are an infinite number of prime numbers.

We remember Euclid 2300 later so he accomplished a lot with his life. Today there is a big market for web pages, microcontrollers for gas pumps and washing machines, missile defense systems, etc. You can keep very busy writing programs for that stuff but it probably won’t be remember in 2300 years. (What’s a gas pump?)

One of the goal of mathematics is to introduce tools that represent problems in a way that is easy to grasp for a human mind. For example, geometry is a good tool to get some intuitions on the problem of classifying sets of data. Also, a well written proof is, by design, easier to check by a human than by a computer.

On the other hand, programming languages are designed first to be easily parsed by computers. With supercomputers, exascale computing [0] is now possible. Yet it is still hard to use fully the power of such computers because what is intuitive for a human mind is not always easy to program. For example the video proof of the inversion of the sphere [1] is checked more easily by a human than by a computer.

Finally instead of using only the power of computers, or only the power of human brains, it is also possible to combine both. This requires to improve the interaction between computers and human beings. In a video on thinking the unthinkable [2], the author notably remarks that the introduction of symbols in algebra allowed human beings to extend the problems they could think about. With better interfaces, the computers could help us to write fuzzy or explicit proofs, but more importantly, they could help us to think.

[0]: https://en.wikipedia.org/wiki/Exascale_computing

[1]: https://youtu.be/OI-To1eUtuU

[2]: http://worrydream.com/MediaForThinkingTheUnthinkable/

Por que no los dos?

There are reasons to prove things and reasons to program things. What is the hypothetical individual trying to accomplish that they can do more via programming than proofs?

Also, as pointed out by others, as of the 20th century we had automated proof systems which have only improved in the 21st century. So someone wanting to prove things can do a lot more now without relying as much on proving "by hand".

When I write math papers I often use proof assistants such as Coq to leverage my programming background to avoid some pencil and paper proofs altogether and rule out many sources of human error. If you consider yourself better at programming than proving, definitely take a look at proof assistants to leverage the former to enhance the latter.

Smart people should write proofs. Less smart people should do the plumbing.

I'm actually betting on the opposite. Better proof systems will allow programmers to accomish many multiples of current productivity.

> Explicit proofs (e.g., in math and CS) are more precise but longer, harder to check, and harder to debug.

Sorry, I've done a LOT in both (1) proofs in pure and applied math and (2) algorithms and software, and your statement is strongly wrong and backwards -- the math is much easier than the computing.

E.g., my Ph.D. dissertation in applied math had both proofs and the results of some software. There was no problem getting errors out of the proofs.

Proofs are really easy to check. I've done thousands of proofs, and I'm not sure I've ever had a mistake in one.

I've written perhaps a million lines of software, and over 50% of the programs had bugs until I found and fixed them.

One of the real advantages, powers, of math is how easy it is to check proofs.

Commonly it is much easier to have a correct and relatively easy to read proof of a math theorem than it is to have a correct and relatively easy to read proof of an algorithm where it is easy to see that the proof and the algorithm are as claimed. Even for just a simple, old algorithm such as Quicksort, it is not easy to prove it is correct; even the notation is not easy. In computing, proofs of correctness commonly have to be in the framework of mathematical induction, and there some notation is needed typically not seen otherwise for the algorithm.

Uh, mathematical induction is to show something is true for all the natural numbers, and the technique basically returns to one of the good definitions of the natural numbers.

Beyond just algorithms, in computing proofs of correctness are so difficult that we essentially give up: The reason is, the assumptions are too difficult to list. If you will, a common problem is "too many edge cases".

It is true that there is something to learn about how to write proofs.

Pure math has a standard that in precision puts it far above essentially all other writing: Some pictures or intuitive explanations may be tolerated but they are not necessary and mostly not wanted. Also, there is no role for "try it and find out", for "doing some examples to see how it goes", some manual manipulation like do when when learning to use socket wrenches or a chef's knife. An old joke was, how complicated a math description would be for how to put on a suit coat.

E.g., a missed definition sticks out worse than a sore thumb. E.g., it should be clear, maybe even mentioned, in the proof, for each of the assumptions, where it got used.

So, the math writing has to give really solid results just from the words and math notation. Bluntly, that is unique in writing.

For accomplishing good, new things, I'm strongly on the side of math with proofs.

The core of my startup is an example. There are no heuristics there, just some math with proofs. Without the math, there would be only guessing and heuristics on how to manipulate the input data to give the desired outputs, and the chances of any heuristics having stumbled onto the same manipulations as provided by the math are zip, zilch, and zero.

E.g., some of the math is close to some math commonly considered, but my math fixes some essentially universal mistakes, really misunderstandings, that have become standard. That is, the common understanding is that there is a fundamental problem there, but that is not true, and my math, with proofs, shows that. Without the math and proofs, I would not have thought of the data manipulations or, if I did, have confidence in their correctness or power.

Sorry, guys: In my opinion, math is the main tool for the most important progress in applying computing to help civilization.