Syzygies

https://github.com/Syzygies/Compare

So you're in a restaurant where you don't speak the language, you can't read the menu, but you see three price points for set meals featuring the house specialty. (Say, "Crossing the Bridge" noodles in Yunnan.) Which do you choose? My tour guide, the author Fuchsia Dunlop, later agreed with me this is obvious: The middle choice.

So you're choosing between Go and C23 as candidate successors to K&R C. They both have "royal blood". One got the name. Knowing nothing more, which do you choose?

The answer is equally obvious. The one that got the name also got the warts.

While Avatar actor Stephen Lang was still in college, he played MacBeth. I brought him news that Birnam Wood had moved, and he drew inspiration from every fiber of my being to deliver his "tale told by an idiot" spiel.

I can still feel the spit hitting my face!

Steve Martin in conversation, 2002. 34:20 to 36:00 is this exact question.

Later, Robin Williams joins him on stage. My cameo starts at 1:01:40, inaudible and off-camera, because I'd traded a seat up close for two in the balcony so my future wife could join me.

People like to make rules. Leave them be in their tree houses, unless you really like to play too. I thought it was a right of passage in high school to laugh at the French forming committees to tell peasants how to speak their native language. We haven't generalized from this example?

Who gives a rat's ass whether this governing body thinks Pluto is a planet or not?

Researchers bought nearby for great housing values and short commutes. My high school was typical working class weak except for an exceptional science program, to support the many "faculty brats" like myself. Half my friends had parents working in the research labs. One day in the 1960's I saw my first computer, sized like a ship's bridge where I played a primitive computer game, two dots orbiting a sun.

My Dad devised the "Bayer filter" for recording color in digital cameras. His best friend played a similar role in video. Long before the internet, the deepest facts about the world came home to me as tales told to my Dad by colleagues in the labs.

My Dad's first experience with a loop was punched cards of a different color, put them back in the hopper and make a mark on a blackboard. These stories prepared me for the inevitability of computerizing my branch of mathematics.

Still, reading this account, I'm surprised so much so soon.

I'm a retired mathematician with a primary research project, and too many tangential projects I fear revisiting; tokens be damned, will they burn all my time? Translate the K&R C computer algebra system that got me tenure to 64-bit modern C. Implement a no syntax macro language to support my Go60 ZMK keyboard. Realize my vision of how interlinear translations should work so I can read Flaubert in the original for an online course this fall. Rejigger my decades-overgrown .bashrc setup and my status, install scripts to manage Bash, Ruby, Lean, Tailscale and my Homebrew setup across four machines. And a waiting queue as these tasks clear.

Fable 5 (with Opus 5 as backup) on Zed with a $200 Max plan has been a sea change for me. Carefully alternating planning and auto modes, I manage all these projects at once using Zed's Threads Sidebar. I'm a virtual CTO taking intense meetings all day, relieved to go cook or run errands when credits stall. Anything I've procrastinated for months is now making steady progress; the translation project I feared taking a month is nearly done with several hours of my attention. My personal IT support is now more advanced and easy to use than I ever imagined possible.

My project creation has been a series of agentic "parenting" steps, so there are years of evolving cultural DNA. I had so hated agent comments that recent agents simply weren't commenting at all, instead recording all context in support documents. We had a "come to Jesus" meeting to discuss what commenting style would benefit both my failing working memory and future agents' token use.

It has taken me two brutal years so far to learn to use AI. AI is a dangerous and powerful Iron Man suit, an extension of our associative minds that is a different experience for each person.

One doesn't ride a surfboard by telling it which way to go. I would surely die surfing a big wave, but my experience with AI doesn't resemble other accounts.

Bar staff don't universally view half pint orders with respect.

How Pixar’s Toy Story 2 was deleted twice, once by technology and again for its own good

https://thenextweb.com/news/how-pixars-toy-story-2-was-delet...

SuperDuper! and Carbon Copy Cloner are as close as you can get to a hot spare. For data drives, interchangeable.

Time Machine's virtue is single file recovery.

Arq is off-site storage. Any hybrid backup strategy can fail under scenarios better imagined than experienced. Now that I'm no longer bicoastal, Arq (and a safety deposit box) saves me if my house burns down.

They both have decades of experience providing astounding support. I should know as an edge case that has tried to rip the wings off of both their programs (trying to migrate away from disastrous RAID software and ending up with duplicate UUIDs, the sort of thing that never happens to anyone else). This matters even if you never need support: Their software is battle-tested by decades of user experience that they understand.

This leads to software convergence, which this rewrite furthers. At first SuperDuper! appeared to me to be oversimplified to avoid trouble at all costs, while Carbon Copy Cloner appeared to be a collection of enthusiast scripts. One could in fact find the scripts driving either; I expanded SuperDuper!'s scope by directly calling an internal script for years.

Decades ago I used Retrospect. They were arrogant twits but they supported external tape drives and such. My breaking point came when when my life turned bicoastal, and their time zone bug forced full backups after every flight. No MBA stereotype could prepare me for the stupid brushoff I heard at a MacWorld show over this. External drives had become affordable enough to motivate a switch to SuperDuper!

More recently there was a macOS release that put the category into crisis, and Carbon Copy Cloner figured it out first. I switched and I haven't looked back. I loved SuperDuper! and I love Carbon Copy Cloner. How much control surface do you want? You have to see for yourself.

Mathematicians believe we're lucky to have been spared the Nobel Prize. While some repeat a discredited story this was because Gösta Mittag-Leffler was sleeping with Nobel's wife, it is generally felt that mixing ego and the possibility of a Nobel Prize has toxic effects on a field.

We now have both the Fields Medal and the Abel Prize, but both pass over the midlife period when ego eclipses talent.

I tried this, long ago. I just wasn't getting Haskell, so I'd retype my programs from memory and reconstruction. Obvious for music, why not for code?

All these untested opinions? You'd think we were discussing BMWs.

What is the purpose of mathematics? To be the architect of new conventions by seeing clearly past the old? If so, believing that the entire point is proving statements is a poor start. Bill Thurston was a visionary who happened to prove a great deal of what he saw, but his influence was his vision.

For those of us who like to understand every line of code we generate, and have labored for years to learn how to make best use of AI, a factor of two is a reasonable estimate for our productivity gain.

For those of us who believe mathematics is about achieving human understanding, having machines decide what's true and what isn't makes a night and day difference. Again, about a factor of two.

I spent far too long comparing dozens of languages, only some of which are part of the above project, before switching from Haskell to Lean for a new phase of my math research. Lean wins for me without considering or using dependent types (for now). It is simply a better programming language than any I have seen.

This is a critical advantage for those interested in proof. One codes tactics using the same language as for proof.

https://github.com/Syzygies/Compare/blob/main/source/lean/Na...

I do have a future interest in proof, giving Lean an edge for me. I prefer my symbolic reasoning in visual form. I anticipate a future where we draw and view AI drawings, and see any printing press derived notation as antiquated as cuneiform. The above image is a possible language for representing the first Lean proof in "The Natural Number Game". About one in ten mathematicians that I show this to can grasp it much faster than the Lean notation. The other nine imagine a visual programming language to be something like a PowerPoint slide or a children's graphics language, and don't see the point.

The obvious question Terry Tao seems not to address: AI mops up our unsolved problems? Whose unsolved problems? The architecture of mathematics will remain a human endeavor long after we replace human construction workers with machines.

Gauss famously summed the integers to 100 in school as a kid. It's a litmus test for mathematicians, ask them how they think he did it.

The sum of cubes 1 + 8 + 27 + ... + n^3 happens to be the square of this formula, making it easy from here. Arrange cubes in 4-dimensional space filling out a shape which is the product of two copies of the above triangle of squares illustrating 1 + 2 + ... + n. In other words, working in wxyz space, the shadow in both the wx and yz planes is this triangle. Now rearrange these cubes to form a pyramid with an n by n by n base directly illustrating 1 + 8 + 27 + ... + n^3.

Mathematics is an extraordinary technical accomplishment allowing people to instrument-fly airplanes with the windows painted over. Some of us, most famously Bill Thurston, prefer to look out the window. This exercise is a great example for "feeling" mathematics rather than working around a failure of cognition using formulas.

AI is putting mathematics into crisis. Soon we'll all have AI technical superpowers, and the only meaningful way any of us can excel is by having actual creative vision.

I didn't see semicolons, but I saw plenty of {} braces, and I can't explain why they're needed.

https://github.com/Syzygies/Compare

"I'm already quite sure how I will die: I'll read another article on Hacker News about a new programming language where I see nothing new, and I'll read that they included {}; to make C programmers comfortable. I'll have a massive stroke."

The 2017 Rohingya massacre in Myanmar? They handed him the death toll. He filed it under growth.

https://xkcd.com/327/

My first example, I was asked to give one more talk on how one needs to shuffle seven times. There were four people, and a blackboard smaller than my kitchen window. I went for it like I was in office hours, which I've always enjoyed more than teaching. A few weeks later a phone call "I liked your talk." "Thank you." "Could you come to Switzerland to give it again? We can only offer a week's full expenses..."

Then I was asked to write a review of the off-broadway play "Proof" for the American Mathematical Society Notices. I didn't read it much, but I was told people do. I worked a very hard week on my review; my Swarthmore College classmate Ben Brantley's Broadway reviews were life or death for productions at the time, and I didn't want to embarrass myself. Ron Howard read my review, went to see "Proof" twice and loved it, and hired me to be the math consultant for "A Beautiful Mind". That was a transformative experience.

Every audience is indeed an audience of one.

https://www.ams.org/notices/200009/rev-bayer.pdf

I'm Ruby or Lean 4.

Lean is designed to be optionally verified; proof is its primary (but not only) application. It seems an impedance mismatch for Jane Street to explore this direction without also migrating to Lean 4.

Various priors inoculate me from feeling some of the rejection expressed in other comments. I knew Sammy Eilenberg, perhaps the most famous mathematician to work at Columbia University. He hired me. With friends, I ran into him one night out in NYC, and in his 70's we all stayed out past dawn. His late career focused on topos theory, and everyone in the building politely rolled their eyes. Those are working mathematicians having an understandable reaction; most reactions to topos theory here are simply uninformed. The evolution of programming languages has lead from the lambda calculus to many forms of category theory. Topos theory would not be a surprise.

The Leech lattice? Could be a brilliant idea. Compare Lenstra's elliptic curve factorization algorithm. Sometimes famous landmarks in mathematics have remarkable properties; mining them for algorithmic advantage is no different than mining asteroids for rare metals.

The involvement of AI is most problematic. Mathematics fears being swamped by mediocre AI-authored papers, but the truth is "publish or perish" has long lead to mathematics being swamped by mediocre papers. Bad artists are losing jobs, but good artists are working faster.

I welcome a new era of programming language design, where AI makes rapid prototyping a reality. We just have to take sharing this work with a grain of salt. Stop reading when you lose interest, but welcome the churn!

I have email locally dating to the dawn of the internet; it's one form of external mind-mapping for me. I'm completely baffled that a decent mail program can't handle the mail for a small town, rather than struggling with one person's life history. This is a question of algorithm choices; performance has to be the top priority. If search is instant, who needs "features"?

That strikes a chord for me. In grade school my teachers could not distinguish between these perspectives, for the standard shoelace knot. I found their method stupid, and they thought my method was wrong. This was but one of many lessons that helped me to learn to think for myself.

She was nevertheless welcome at a frequent flyer event hosted by Continental in Houston, where she beat me at poker.

In Bordeaux, winemakers consider themselves geniuses manipulating a many variety blend. In Alsace, winemakers view their role as not screwing up God's work.

AI agents fielded by major AI players still fail at the basic task of providing immediate and correct support for use of the current versions of their products. If a programming language is too new to have adequate representation in the training corpus, there isn't an accepted standard way to provide a reference manual targeting AI agents. Even the best way to include documentation in a large project so new AI agents can take over is controversial. A pile of linked markdown files really isn't an answer, less structured than a codebase itself, that AI is good at navigating.

Other HN posts have discussed using SQL as a backbone for the AI "mind mapping" support we need for AI more critically than for ourselves.

I was hoping that CQL could be an answer to this. Perhaps, but not its current primary goal.

    UFBT: Unofficial Flipper Build Tool (installation guide)

    uFBT is a cross-platform tool for building applications for Flipper Zero.

I'd love to extract just the foreign language from Pimsleur foreign language lessons, for faster review before trips. Your pipeline has many elements in common for what would be required.