My response is too long for HN; breaking up into two parts :)
Part 1:
==============
I feel like there is a survivorship bias in your assessment: the students who would benefit from learning to construct a rigid argument without holes are already the ones who can hand-wave their way to the result, i.e. they already have the motivation and intuition to get there.
On the other hand, I feel like over 9 out of 10 people who could and would enjoy advanced mathematics get turned off by unnecessary formalisms some time in highs school (Lockhart's Lament describes vividly how Euclidean geometry there is massacred - and that's both the first, and often the last time they see proofs!).
To add insult to injury, rigid reasoning is not introduced to students unless they are math majors, and even then, it's when they take a Real Analysis course. The way we teach intro Calculus and Linear Algebra classes should be classified as a Geneva Convention violation and a crime against humanity: all the intuition you can get from a Bourbakism with none of the rigor.
It doesn't need to be this way. Even rigor can be fun. Just like everything else, rigor is a part of mathematics that we do for a reason. Once you approach the very concept of rigor the same way you approach, say, derivatives, you will see that there is no need to impose it on people.
How many times have you seen a "proof" that 0 = 1, usually derived from a coy division by zero, or abusing square roots, etc? People repost those on Facebook as memes. They are fun!
But also, they are the motivating example for rigor. After all, that's the entire reason we need it in the first place: to avoid arriving at incorrect conclusions.
Without having a vast assortment of examples of arriving at incorrect conclusions, rigor is both unmotivated and unnecessary. Newton and Leibniz didn't need rigor when they invented Calculus, after all; hand-wavy infinitesimals did just fine. Why should the students bother?
There is no value in rigor in and of itself. All the effort to put mathematics on a rigorous footing gave us are things like Banach-Tarski Paradox (which is, objectively, absurd and only shows that the extent to which math models physics goes so far!) and Godel's Incompleteness Theorem (which shows that even attempting to reach Perfect Rigor is futile).
You don't need to introduce Peano's axioms to talk about number theory, and neither does any number theorist, really. And we wouldn't want any student to crank out a Principia while working on their topology homework.
So, treating rigor as a branch of math (which it is!), it needs to be introduced and taught just like any other branch - starting with context, stories, pitfalls, and seeing all the motivation for why we do things the way we do.
It starts with basic critical thinking, logic and philosophy classes, where people learn the difference between "All liberals support free healthcare" and "All supporters of free healthcare are liberals" (....well, I wish).
Going further, it's seeing the "proofs" that 0=1, or that all cats are grey (by induction). The latter "proof" is still the only thing that motivates me to check the "obviously true" things, like the induction step being applicable to the base case.
In high school, I had a great little book called "Lapses in Mathematical Reasoning" by Bradis and co-authors. It was a perfectly accessible assortment of gotchas.
Zeno's paradoxes are a motivation for some of the rigor of Calculus (convergent sequences and infinite sums are the answer to the paradox).
And when we look at rigor like this - like a thing that needs to be motivated, not an a-priori good - we see a rather disturbing pattern that rigor has been introduced at the expense of clear reasoning.
Take Calculus. Teaching it with limits, epsilon-deltas, etc. without giving a motivation for why this complex machinery is needed is purely a waste, and a thing that made many people despise math (it turned me off from analysis for a very long time, personally).
The problems that this rigor addresses aren't even taught to the vast majority of people who take Calculus! Everything that the intro course covers can be taught with infinitesimals just fine without introducing the epsilon-delta rigor.
And, in fact, epsilon-delta rigor can be entirely dispensed with (because the infinitesimals can be put on a rigorous basis, with non-standard analysis). Epsilon-delta was not an achievement. It was a defeat. It was the greatest minds of the time not being able to figure out how to add rigor to the concepts that Leibniz and Newton introduced, and so they simply powered through and worked around the concept of infinitesimal to make some hairy math work.
With rigor, just like with anything else, we have to ask: what's the return on investment there? Is it a good bang for the buck? Why is hand-waving bad?
Having learned a subject, we know where hand-wavy reasoning can lead. We know that not all cats are grey, or that continuous function doesn't need to be differentiable anywhere.
But there is no value in rigorous reasoning in Calculus if we are not running into monstrosities like the Weirstrass function. And, when we start out, we don't - because the Nature is quite nice, math-wise. At least on a day-to-day scale.
Adopting Arnold's mindset, the amount of rigor in a mathematical argument is somewhat like the amount of precision in a physical model.
No sane person would start teaching physics with Einstein's relativity. But in math, not only we do that, we never teach Newton's Laws - and in introductory classes, we don't even explain the formulas!
Imagine forcing high-schoolers crunch Einstein's tensors where all they needed was F = mg, without ever explaining what curvature even is or why it's needed ("it'll come in handy, trust us").
This is what we do with Calculus - or in any area where rigor is used without justification.
>Then, once you have written your stuff in that dry style, you can add some glimpses of discourse that become much more valuable than if you had started with some informal hand-waving
You always start with some informal hand-waving. Not including it in your paper is, put simply, lying by omission.
And great mathematicians didn't shy away from prose, especially when introducing significant concepts. When I was trying to understand quaternions, I found all the texts I looked at stupefying - until I found Hamilton's book where he introduced them.
Not only I got more from the first chapter than I was aware there was to know, but I also learned things like where the word vector comes from when we use it to mean "a magnitude and a direction". Learning it was infinitely more valuable to me than seeing the axioms of a vector space (which, of course, you never need to remember - just write down a handful or so rules that translations in a plane satisfy, and the chances that something that fits ain't a vector space will be zero unless you go out of the way to make up a contrived example just for that purpose).
In fact, and that's Arnold's point, you lose no rigor by ditching formal reasoning when you can be concrete.
I believe that it is detrimental to the human brain to go through the exercise of "proving" that a collection of invertible operators, along with all their compositions, form a group.
And yet, this is a common exercise! People spend time on this! Just watch: [1]. The video goes for seventeen minutes! For diagonal matrices with non-zero entries!
I feel that having this "rigor" is worse than saying that these matrices form a group because of course they do.
On the other hand, no time is ever spent explaining why the formal definition of "set with an operation" is introduced. That's because it's needless, of course; it seems that the sole purpose of this definition is to create exercises.
=====
[1] https://www.youtube.com/watch?v=q_JqHQPbmUk
[2] https://math.stackexchange.com/questions/919040/proving-a-gr...
[3] https://math.stackexchange.com/questions/1108349/prove-that-...