I strongly recommend against auto-squashing. It creates large commits without the semantic intent of the author. In a large PR, you want clean, small, semantic commits, which makes it much easier to review and understand.
Becoming very comfortable with "rebase --interactive" and other cmds for editing your (local!) history before merging helps a lot. Once you are, it only adds 5m or so of extra work to most PRs. And while acquiring this knowledge used to be difficult, LLMs make it very easy these days.
I would add that (related to your "maintainability" point) ensuring the code is as simple as possible, and thus much more likely to be "debuggable by review", is a goal of review. Even that won't prevent bugs in the absolute sense, as you rightly say, but it boosts your probabilities.
It's a good practice. Worth mentioning also: the same can be done with ordinary git log, assuming everyone is using git well. A proper git log of yesterday's work can be like your work newspaper with coffee.
Yes, at the prodding of the reviewer (from wikipedia):
> After the announcement, Nick Katz was appointed as one of the referees to review Wiles's manuscript. In the course of his review, he asked Wiles a series of clarifying questions that led Wiles to recognise that the proof contained a gap.
It seems likely Katz played a crucial role here.
Wiles is just a prominent example. In practice, other humans often play this "verification role" for mathematicians, whether via a formal review process or informal discussion.
> It would be great if someone could explain to me how AI improves this situation.
It's main utility is in the search step, not the verification step. The search is the bulk of the work and creativity. Separately, as the sibling commenter pointed out, it will likely get better at the verification step as well, with integrations of tools like Lean.
> One hallucination in 300 steps of logic is enough to destroy the entire proof.
The situation with human mathematicians is not much different. Eg, Wiles original proof of Fermat's Last Theorem contained errors found by reviewers, which he later repaired.
I found a lot of interesting, if speculative, thoughts in the article, but...
> Superhuman means unverifiable
is not true for at least large classes of problems. The recent solution of the "unit distance" problem comes to mind, or any future AI-solved math problem that was beyond the capabilities of humans. You can tell it's superhuman (it's doing things humans can't) and you can easily verify its results are correct.
For other classes of problems (eg, policy suggestions for large scale systems like the economy), the point is fair.
Yes, this is true. And is a bigger problem on large teams. One mitigation is a comment by the original author at both sites that there may be a coupling in the future.
But, again, the point is that you don't know yet whether you have a single source of truth or not. It's a question of the relative badness of duplication vs premature abstraction in cases where the code may diverge or converge in the future. There is no generic answer. But as a heuristic, based on my personal experience, I have always found premature abstractions to be more painful to work with. Even more so when someone else has authored them.
> I believe that "single source of truth" is a principle that should always be followed
Fundamentally, the article addresses cases where it's not clear yet how many sources of truth there will be. Are the two spots in the code using the same algorithm, or slightly different versions? More importantly, will they change for the same sorts of reasons?
The title adage (correctly, imo) argues that making two different things the same will cause you more pain than making two same things different via duplication. In the latter thing case, the "damage" is just having to make the same changes twice, or doing a refactor to introduce the abstraction. In the former case, you have to keep adding to your abstraction, or undo it. Most crucially, it breaks "locality", which is the only property you really care about when making changes. I just want to make this change and not worry about side effects to unrelated parts of the system.
Assuming this pans out, every other professional linguist in the world has had the option to use Claude or other LLMs, but has not solved this problem, despite the incentives for doing so. It stands to reason the human is adding crucial value.
> What possible use could there be for doing this?
Early detection of disease, as well as every kind of physical issue with the body you can imagine.
The incredulity of the question seems rooted in the medical culture of our current time. It's easy to imagine a science fiction future where scans happen not every 9 months, but daily, in your home, and the idea of not constantly checking your full body would be as strange as not brushing your teeth is to us...
Anecdotally