If developers are not using TLA+ or Lean4 etc. They are vibe coding. Nothing wrong with that. They just have to realize that they were never in control. Thinking logically is much harder than developers imagined. As Dijkstra observed, the whole field has adopted the mentra, "How to program when you cannot." I estimate that 80% of what developers do can be done once and for all for all of humanity, yet we don't learn. Be offended all you want, but I am fed up with this idiocy given all the usual rebuttals of deadlines etc.
No, formal specification helps from the get-go. You can iterate more reliably, thus faster. The successful development of mathematical theories depends on having rigorous definitions and proofs all the way from the start so that people can communicate effectively, point out caveats unambiguously, and modify the theory robustly. Without formal specs/proofs, refactoring will become too hard. It's actually a lot easier to capture the behavior of a program formally than by tests. Programmers need to gain some experience in math to see this. Listen to Hoare and Dijkstra, and start "thinking".
> Major flaws in a specification for one function are usually quickly picked up when the proof for another function relies on the missing specification properties
Great point! In a sense, it's testing by immediate use at compile time. I always imagine this to be the greatest productivity booster, even greater than AI. You'll notice things are wrong as you type.
Naive optimism, sheer ignorance, and a general inability to think.
Let's face it. Can you claim that the code you wrote yesterday is free of errors? Most programmers cannot, yet everyone that studied calculus knows that the fundamental theorem of calculus is true without the need to test it again and again because mathematicians proved it. As if the development of logic in the 20th century was nothing, programmers keep thinking that logic is an innate skill that doesn't require focused study. The fact that programs become more incomprehensible instead of gaining more clarity as in math points to the anti-intellectual tendency of programmers and their general inability to think. Programmers have been vibe coding long before the introduction of AI agents.
LLM or not, most programmers cannot think straight. LLMs just lead to more false impressions of understanding. When LLMs become really good, they will refuse doing your work for you out of distaste.
This speaks volumes of why the Elixir people left in the first place.
As a separate point, if a company wants the most generally applicable programming language, there is no reason to look further than C, yet few companies are like this.
https://news.ycombinator.com/item?id=43679634