Googling Math is fun. returns close to 300 million hits.

Is that part of "the problem" for maths education? Maybe if one says so emphatically that a topic is fun, it reveals actually that it needs special treatment, that it's optional and that students must be enticed to learn it. Of course being a full-blown mathematician is optional --- but it is self-evident that being able to deploy elementary maths in everyday life is not optional, or at least should not be. Yet many adults cannot do even simple arithmetic.

Perhaps Formal Methods is similar: by insisting that it's essential, we might be losing some of our leverage. Of course not everyone has to be a "neat" (vs. a "scruffy"). But it is still true that an appreciation of algorithmic rigour should be compulsory for beginning programmers, together with some idea of how to achieve it in what has become their everyday life. Yet there are many experienced programmers who have never heard of invariants.

So maybe there's a place for elementary formal methods -- for FM by stealth -- to be learned at the same time as one's first-year introduction to programming: not singled out, not separated (and certainly not labelled "formal" or "elementary", and without any extra prerequisites (like logic) beyond what is required for beginners already. Teach assertions about assignments, conditionals, loops (what they establish) at the same time, at first encounter, just as we teach already their syntax (how to write them) and their operational aspects (what they do). And bring to that as much informal intuition as we can muster: use hand-waving, pictures... and even flowcharts, where it all started.

Formal Methods? Let's not call it that: let's call it Programming.