Darcs' Theory of patches | Hacker News Reader

Darcs' Theory of patches

darcs.net

20 pointsvorador8 comments

Let me define pseudo-math to be the approach of making a few mathematical definitions and then proving only some trivial "theorems."

Theorem. The Darc's theory of patches is pseudo-math.

Proof. By definition. QED

Personally, I kinda like watching physicists get slightly peeved when you point out that their models could stand being a little bit more rigorous. I mean check out this paragraph:

"""I think a little background on the author is in order. I am a physicist, and think like a physicist. The proofs and theorems given here are what I would call ``physicist'' proofs and theorems, which is to say that while the proofs may not be rigorous, they are practical, and the theorems are intended to give physical insight. It would be great to have a mathematician work on this to give patch theory better formalized foundations."""

Which translates to: you know what, we both know this is all pretty much correct and if you think you need to spend a couple more hours (or days) setting down the mathematical foundations in excruciating detail be my guest, but I'd rather read a thousand papers on string theory.

I mean, I pretty much agree. After all, I studied computer science. We make physicists look pretty rigorous.

Formal computer science usually has more formal proofs than most branches of mathematics. Computer scientists will lay out an explicit proof by induction where most mathematicians will simply write "by induction". At least that's been my experience.

Honestly, it's not a stretch to say computer science that most of us practice day in and day out, and the way most of us study it in college, is heavy on practice and light on theoretical rigor.

I found that to be quite the opposite. Having finished my CS degree and taken various analysis of algorithm classes I found proofs to involve lots more hand holding and shortcuts.

I'm working on finishing my Mathematics degree and proofs are much more vigorous.

Check out some papers on type theory. They prove the most trivial things in excruciating detail.

In principle, I agree that sometimes sacrificing rigor for clarity is justified. But in the case of the Theory of Patches, not a lot of people have managed to understand it in detail. (I say this based on about a year of lurking on the darcs-users mailing list, some time ago.) If in addition to being opaque it's also not rigorous, that's a bit of a shame.

That takes nothing away from darcs as a piece of software, though. You don't have to understand the theory in order to use the tool, and it really introduces a revolutionary way of thinking about version control.

In addition to not being rigorous, it's utterly trivial stuff. This is like making string concatenation difficult by calling it a monoid.

Reply on news.ycombinator.com