> 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 a

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