Three new papers on AI, verification, formal methods and the risks of vibe coding

In this issue: temperature conversions; risks and power of metaphors; AI and verification; rewarding publishers and authors.

No one asked, but you get it anyway

Some countries have their quaint, charming traditions, which can be disconcerting to the newcomer.The one I have in mind at the moment is the US with its bizarre system of units. Temperatures, for example, are displayed in something called “Fahrenheit”, incomprehensible to anyone not raised in the local culture. To convert requires prodigious mental calculation capabilities. You are supposed to subtract 32 (beware the carry!), then multiply by 5/9. Who ever divides by nine? Talk of cruel and unusual punishment.

Fortunately, you do not need to torture yourself when you see, for example, a “70” display. Just memorize the following 4-step procedure:

Subtract 30. A round number in tens, always easy.
Divide by 2. Also immediate.
Add 10%. Again trivial and instantaneous.
Subtract 1. Easiest.

You may want to go through this list a few times to make sure you remember it, and after that applying it is a breeze.

For example, 70 → 40 → 20 → 22 → 21. The exact answer (from the formula (n - 32) * 5 / 9)) is 21.11.

In fact it is easily shown that for all naturally occurring terrestrial temperatures the error is less than $0.3^\circ \text{C}$ !

The result is exact for $0.3^\circ \text{C}$ F (10 $0.3^\circ \text{C}$

Just take the time to learn the four steps above and forever forget having to think about carries and non-trivial divisions.

(The transformation from Celsius to Fahrenheit is just as simple — left as an exercise until next week.)

Choose your comparisons

The debate continues to rage as to what AI and vibe coding in particular mean for employment. A recent viral Twitter post by Matt Shumer, viewed (supposedly) 73 million times, raised the alarm to a new level.

Obviously there will be more discussions of this forefront issue in forthcoming issues, but here I will just highlight here a specific point. The danger of metaphors and clichés in reasoning is well known. For example, you have started a project, are encountering difficulties, and wonder whether you should go on or give up. One piece of advice is “Do not change horse in midstream!”. In other words, go on. Another is “When you find yourself in a hole, stop digging!”. In other words, give up and cut your losses.

No one of the metaphors is particularly useful. Each tells you more about the mindset of the person using it to give advice than helps you decide rationally. What matter is the choice of metaphor.

For some reason, software people are fond of car metaphors. I have heard them for decades, used to argue lots of points and their opposites. When we talk about vibe coding, what is the right car metaphor? Let us say we have a 5-fold improvement in technology. If it is in car technology, what effect will it have on the future of drivers? If we are talking about ordinary drivers, for example taxi drivers, it will level things down: whatever advantage an excellent, seasoned, expert taxi driver had on others will pale in comparison to the leap that everyone is now able to take. Their advantage disappears! On the other hand, if our metaphor involves Formula-1 drivers, the best ones will be able to make the technology work to their benefit and increase any edge that they already had.

To get your foregone conclusion, pick your metaphor.

For vibe coding I pick Formula-1. In advanced countries, ordinary programmers did not, pre-AI, have much of a chance already: the easy or repetitive jobs have gone to outsourcing. At least in the short term, those having most to fear from AI are the outsourcing companies, rather than skilled developers. Someone must drive the AI, write requirements, check results, catch hallucinations, direct the tools to correct their mistakes.

I find that most discussions, including from people who really know what they are talking about (say, Andrej Karpathy) miss the major issues identified in my “From Probable to Provable” paper (not yet published in Communications of the ACM, I have no idea when it will reach the top of the queue, but of course available as a preprint), in particular requirements engineering and, to fight hallucinations, verification. The need for people competent in these disciplines will not cease to grow.

The Interplay between AI and verification

The mention of the last topic is an opportunity to remind readers of the forthcoming workshop on The Interplay between Artificial Intelligence and Formal Verification, near Toulouse, 8-11 March 2026. The list of accepted papers (soon to be turned into a schedule) is available at the workshop page. Even a quick look at that list will show that we can expect a fascinating meeting. The spirit is collaborative and one of the activities will be to engage as a group in crowd-coding-plus-verification.

Priority for participation is for the authors of accepted presentations, but there are a few slots available for others interested in participating. The registration form is on the event's page.

Giving publishers and authors their due in the age of AI

With this issue of the newsletter I am coming back to the regular schedule (Sunday night). The timeline has drifted a bit recently as I have been devoting significant effort to an exciting project: ensuring that publishers and authors of valuable Web resources get their fair rewards, financial as well as reputational, from the use of their work by LLMs and other AI “aggregator” tools.

Next week's issue of the newsletter will be devoted to this project, Recognyze, but you may already take a peek — particularly if you maintain any web resource, such as a site or just a blog, or just contribute articles to such sites, or publish books etc. — to the Recognyze site: recognyze.ai. (Hint: look up the “AI index” for authors.)