3 ms·

I started with SML in the 1980's, implementing a core math algorithm (Grobner bases) used in my K&R C computer algebra system Macaulay. Then I got this idea the

I started with SML in the 1980's, implementing a core math algorithm (Grobner bases) used in my K&R C computer algebra system Macaulay. Then I got this idea there should be a related algorithm in a different problem domain (Hilbert bases) and I managed to convert my code in twenty minutes. It ran. This completely blew my mind, on par with switching from punched card Fortran to an APL terminal in the 1970's. Everyone talks a good line about more powerful, expressive programming languages till they need to put in the work. Ten years effort to program like ten people the rest of your life? I'm 69 now, I can see how such an investment pays off. I moved to OCaml. Studying their library source code is the best intro ever to functional programming, but I felt your "all the way" pull and switched to Haskell. (Monads make explicit what a C program is doing anyway. Explicit means the compiler can better help. What it comes down to is making programming feel like thinking about algebra. This is only an advantage if one is receptive to the experience.) I'm about to commit to Lean 4 as "going all the way". Early in AI pair programming, I tested a dozen languages including these with a challenging parallel test project, and concluded that AI couldn't handle Lean 4. It keeps trying to write proofs, despite Lean's excellence as a general purpose programming language, better than Haskell. That would be like asking for help with Ruby, and AI assuming you want to write a web server. I now pay $200 a month for Anthropic Max access to Claude Code Opus 4 (regularly hitting limits) having committed to Swift (C meets Ruby, again not just for macOS apps, same category error) so I could have first class access to macOS graphics for my 3-manifold topology research. Alas, you can only build so high a building with stone, I need the abstraction leverage of best-in-category functional languages. It turns out that Opus 4 can program in Lean 4, which I find more beautiful than any of the dozens of languages I've tried over a lifetime. Even Scheme with parentheses removal done right, and with far more powerful abstractions.

pmarreck 1y ago
Have you looked at Idris 2? I'm 53, impressed that you're still going at it at 69!
- Syzygies 1y ago
  Yes. I'm impressed with Idris 2. I love how it uses Chez Scheme, my favorite scheme implementation. I contributed for a bit to getting Idris installation working on Apple Silicon Macs based on Racket's port of Chez Scheme, only to learn that I was working with Idris instructions that hadn't been updated. Lean 4 is a better supported effort, with traction among mathematicians because of the math formalization goal. I have more reasons to want to learn Lean 4. Peel away their syntax, and Lean 4 proofs are the word problem for typed trees with recursion. I find the reliance of AI on artificial neurons as arbitrary as so many advanced life forms on Earth sharing the same paltry code base for eyes, a nose, a mouth, and GI tracts. Just as many physicists see life as inevitable, in a billion runs of our simulation I'm sure AI would arise based on many foundations. Our AI fakes recursion effectively using many layers, but staring at the elementary particles that make up Lean proofs one sees a reification of thought itself, with recursion a native feature. I have to believe this would make a stronger foundation for AI. I don't get that same rush looking at Idris. Using Lean 4 for general purpose programming? It must be good training.
  - pmarreck 1y ago
    I'll have to have a look at Lean 4 then. The simulation hypothesis has a flaw IMHO- If it is modelable and therefore computable, it may be subject to the halting problem

pmarreck 1y ago

Have you looked at Idris 2? I'm 53, impressed that you're still going at it at 69!

Syzygies 1y ago
Yes. I'm impressed with Idris 2. I love how it uses Chez Scheme, my favorite scheme implementation. I contributed for a bit to getting Idris installation working on Apple Silicon Macs based on Racket's port of Chez Scheme, only to learn that I was working with Idris instructions that hadn't been updated. Lean 4 is a better supported effort, with traction among mathematicians because of the math formalization goal. I have more reasons to want to learn Lean 4. Peel away their syntax, and Lean 4 proofs are the word problem for typed trees with recursion. I find the reliance of AI on artificial neurons as arbitrary as so many advanced life forms on Earth sharing the same paltry code base for eyes, a nose, a mouth, and GI tracts. Just as many physicists see life as inevitable, in a billion runs of our simulation I'm sure AI would arise based on many foundations. Our AI fakes recursion effectively using many layers, but staring at the elementary particles that make up Lean proofs one sees a reification of thought itself, with recursion a native feature. I have to believe this would make a stronger foundation for AI. I don't get that same rush looking at Idris. Using Lean 4 for general purpose programming? It must be good training.
- pmarreck 1y ago
  I'll have to have a look at Lean 4 then. The simulation hypothesis has a flaw IMHO- If it is modelable and therefore computable, it may be subject to the halting problem