HN user

Syzygies

3,912 karma
Posts1
Comments721
View on HN

Rich Hickey has a joke about semi-colons in language design

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."

I've spoken before a thousand several times saying with a straight face "Every audience is an audience of one."

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 nearly adopted OCaml for my current math research, in no small part because of Jane Street contributions. I instead chose Lean 4, as LLMs became able to help code in Lean. I give up a factor of two in performance (a gap likely to close) for what reads to me as the clearest expression of each algorithm. Lean is a beautiful language that makes OCaml read like Old English.

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.

As a mathematician, this reads to me as the most informed comment.

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!

Ten Years of Franz 2 months ago

Thanks for saving me the time.

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"?

There's the finished knot, and there's his way of tying it, which is easy to grasp.

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.

Continental Airlines had an active frequent flyer community. A student emerged as a legendary figure (think "Hunger Games") after she noticed that Continental announcement URLs were numbered sequentially, and a not-yet-released announcement rather unfavorable to current elites was there for anyone to read. Quite the brew-ha-ha. Continental retreated.

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

Stop Ruining It 2 months ago

There is a meaningful design axis here, how one views one's role.

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

We have not yet converged on a best (or even adequate) way to present a structured mountain of information to AI, not already in its training corpus.

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.

Not everyone expects to appear on HN, but chasing links this is a par two golf course:

    UFBT: Unofficial Flipper Build Tool (installation guide)

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

Yes, I was going to guess semantic embedding from playing around and seeing the search responses. Thank you for "About this project".

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.

J is unclear on the concept, it's a hack to port APL to ASCII. I'm typing on a ZMK keyboard now where an APL unicode layer would be trivial. There are modern APLs. One can code a iOS keyboard with AI help.

While a native APL would be nice, the cloud solution would be robust access to a professional product. Build the chain via existing tools to bridge the iPad to APL running on a desktop machine.

I looked into this recently; but I've decided on Lean 4 as the successor "best language in existence" for my needs.

My recent language comparison: https://github.com/Syzygies/Compare

My APL one-liner story: https://news.ycombinator.com/item?id=27460887

Julia is reasonably fast. I returned to a language comparison project specific to my math research, to see how I might do better. My agents and I studied the advice in the post and various more recent links from the comments, but we were already mostly on target and nothing left moved the needle.

My work is more combinatorial. Julia does excel at numerical computation. There's a tribal divide in math between people who can't go 30 seconds away from the real or complex numbers, and those whose tolerance is about that long. I try to keep an open mind, but I'm closer to the second camp. Julia is good enough to consider either way.

A development in recent months, AI can assist in general purpose Lean 4 programming, no longer getting confused by the dominant proof-oriented training corpus. If one is a functional programmer who believes that Haskell was on the right track, then Lean is the most interesting language choice for shaping one's thoughts. Benchmarks are inherently misleading if a better language makes it possible to express algorithms out of reach of more primitive languages.

https://github.com/Syzygies/Compare

            C++  100    13.08s  ±0.08s
           Rust   99    13.16s  ±0.02s
          Julia   90    14.54s  ±0.01s
             F#   90    14.54s  ±0.04s
  Kotlin-native   88    14.79s  ±0.01s
         Kotlin   86    15.18s  ±0.01s
          Scala   79    16.50s  ±0.08s
   Scala-native   76    17.14s  ±0.02s
            Nim   65    20.17s  ±0.01s
          Swift   64    20.54s  ±0.04s
          Ocaml   52    25.38s  ±0.04s
           Chez   49    26.64s  ±0.02s
        Haskell   37    34.96s  ±0.06s
           Lean   29    45.39s  ±0.15s

I have thousands of dollars of mechanical keyboards I could sell on eBay, if only I wanted to take the time to remember how I last left the firmware reset sequence.

I set them all aside for several Leopold FC660C Topre keyboards with the Hasu mod supporting QMK firmware.

Then I started getting ulnar nerve issues, either the gym or too many AI prompts. I discovered MoErgo's keyboards, and their custom Cherry Blossom switches. I honestly believe they have subtle design genius pervading their work, beyond anything I have ever experienced. Quiz me; I've also tried X.

Their Glove80 could use a bit of the "door slams like a Rolls-Royce" quality that many of these bespoke keyboard makers apply to more conventional designs. The design nevertheless triumphs.

Their second generation Go60 is my "Stay60" I can't give up. The build quality, and I don't want more keys.

At first it feels like the Cherry Blossom switches fire from a breeze with the window open. One adapts.

Any benchmarks? I have a combinatorial enumeration comparison project where the .NET jit optimized my hot loops for F# to in some cases matching Rust performance. F# is inspired by OCaml, and for me F# runs twice as fast.

Scala got a face lift where indentation replaces syntax, a modern poetry look many of us can't live without. It is entirely practical to eliminate most parentheses from Lisp (I have written thousands of lines of Scheme this way, hands down my favorite code to read), but doing so will lead to a tribal swarm attack. It is also easy to train Common Lisp to lay off the caps, but any stock installation greets users with an old man shouting (GET OFF (MY LAWN)).

The idea of Lisp is pure genius. One wonders where we would be today if any Lisp took a more pragmatic attitude towards encouraging adoption.

LLM's are an extension of us. We sometimes have to work to learn something new; so do LLM's. It's all in how we manage that process. Reifying information is the whole ball of wax, what separates different people's success rates using AI. AI is more surfboard than self-driving car; you don't just tell it which way to go.

I still can't get AI to code well in Lean 4, but I'm writing a parser for a language that doesn't exist. AI understands the language as well as I do.

The common theme is diverse notions of a language. When I order from a menu, I don't order based on price, but I prefer to see the prices.

Lean 4 is the most interesting language on my list. I didn't reject it on price.

Thank you. I will try your Chez idea. I love Chez, even if coding in Scheme can feel like rubbing sticks together to start a fire on an island, when e.g. Scala has induction ranges. And I didn't try Idris or Racket as they compile to Chez, but perhaps they do so better than I did.

As for parallelism this is a primary concern of mine, and I tried multiple approaches for every language where there was a choice. I used my own work-stealing code only when it beat standard libraries. AI warned me I was in over my head, that writing such a library takes years of experience, but my use case (and my expected use cases in my research) is so uniform that simple can win, minimally touching the required bases such as permuting tasks to avoid false sharing.

I don't believe that the JIT languages (F# on top) do so well because of better parallelism. This is branch optimization. For this use case an AOT compiler with ample benchmark data to influence output should do better. That isn't a thing, and the argument seems to be that few use cases stay consistent. A JIT can adapt.

I recently revisited a language comparison project, a specific benchmark tallying the cycle decompositions in parallel of the 3,715,891,200 signed permutations on 10 letters. I kept a dozen languages as finalists, different philosophies but all choices I could imagine making for my research programming. Rather than "ur" I was looking for best modern realizations of various paradigms. And while I measured performance I also considered ease of AI help, and my willingness to review and think in the code. I worked hard to optimize each language, a form of tourism made possible by AI.

The results surprised me:

             F#  100    19.17s  ±0.04s
            C++   96    19.92s  ±0.13s
           Rust   95    20.20s  ±0.38s
         Kotlin   89    21.51s  ±0.04s
          Scala   88    21.68s  ±0.04s
  Kotlin-native   81    23.69s  ±0.11s
   Scala-native   77    24.72s  ±0.03s
            Nim   69    27.92s  ±0.04s
          Julia   63    30.54s  ±0.08s
          Swift   52    36.86s  ±0.03s
          Ocaml   47    41.10s  ±0.10s
        Haskell   40    47.94s  ±0.06s
           Chez   39    49.46s  ±0.04s
           Lean   10   198.63s  ±1.02s
https://github.com/Syzygies/Compare

I'm a retired mathematician hoping to finish a second proof of a major theorem before I die. AI needs to understand my math and help me code. What I spend on AI isn't going to deplete my retirement savings.

So far, Opus 4.7 seems a bit smarter than Opus 4.6 for my use case. That's my only concern. Is an $80 bottle of wine a better value than a $20 or $40 bottle of wine? Pretty much never. If there are those of us willing to buy $80 bottles of wine, of course the market will facilitate this.

People can use whatever model they want. I'm too worried about worms crawling through my dead body to waste time on any but the smartest model any moment can offer.

There are many duality theories in mathematics where both of these perspectives are valid. Each instance is "Duh! What's going on here is just..." and the pragmatic move nimbly through each instance without concern. For others, the potential theory IS the object of interest. Is this apparent pattern a deep principle or just a mirage? When something is actually going on, one learns powerful new techniques by recognizing a precise pattern.

I've stumbled onto deeply disguised dualities in my career. (One could argue with a straight face there are only two, but this is not formalized.) It's more a psychological process than a technical one.

It's always possible to ignore that one is standing in a tree farm. Trees have such interesting bark.

It comes down to are you reading to write, or reading to think?

Zettelkasten facilitates publication dysentery, which is already out of hand. I have the same problem with conventional bibliography managers. I have a few thousand papers and books on my computer, woven with the beginnings of a mind-mapping system. I recoil every time I consider using software "designed" for this, which excels at cranking out papers but not at deftly flying through idea space. And idea space is an actual thing now, that "King - Man + Woman = Queen" linear algebra supporting AI. Ignore this and one is selling buggy whips.

Reifying memory is the next frontier for LLMs, with many efforts underway. That should be our defining use case for mind-mapping.