black_knight

5 ms·

31.
by black_knight 2mo ago
I am not claiming you cant write buggy code in Haskell! But following good functional style, your bug will more likely be compartmentalised, and fixing it will not break some other part of your program.
32.
by black_knight 2mo ago
Dependent types is one possible direction. Not sure when a language with dependent types will arise which will be useful for making real programs. Agda is the most mature dependently typed programming languae (having been around since the 9
33.
by black_knight 2mo ago
This is where I believe strong typing (like, Haskell-strong or stronger) and functional programming in general will be a win. The confidence I have that my fixes are localised when fixing Haskell code is infinitely stronger than fixing even
34.
by black_knight 2mo ago
I am not really sure what Claude meant, but you are not too far off, from what I understand. I have several similar folders with variants of a construction, but taking differently structured input. They are named “plain”, “fibred” and “inde
35.
by black_knight 2mo ago
This was actual Claude output on my screen at the moment I was reading this thread. No hyperbole! As far as I can tell "the capstone" is what Claude usually calls my current goal if it thinks it is a satisfying result.
36.
by black_knight 2mo ago
I have a PhD and can confirm. Oftentimes, the stuff which comes out of Claude is just impenetrable because it invents jargon on the fly, and uses verbs in the most atrocious ways. "The fibred side folded its capstone into the existing
37.
by black_knight 2mo ago
I don’t think this is actually true, though. In fact, I believe the opposite. My experience with LLM assisted coding is that I need a technical hand on the steering wheel to get something workable out it. Otherwise, what comes out is a brit
38.
by black_knight 2mo ago
It is not a hobby when you are paid to do it! But I take it you mean “Done for the art of it”. Which I guess is a concept foreign to many. A few different reasons why use an LLM when mathematics is done for its own sake: Formally verifying
39.
by black_knight 2mo ago
The first sentence of the abstract gives a motivation: "λλ uses a linear type system to encode the physical constraints of optics, rejecting unrealizable programs at compile time." The fact that it its own language does not preclu
40.
by black_knight 2mo ago
I just replaced git clone with a script which fetches the README.md and sets of a fleet of agents to do a cleanroom reimplementation. Lets me ignore the LICENSE.md file, and use how I want.
41.
by black_knight 2mo ago
I saw a fascinating talk by Clément Pit‑Claudel on closing this gap. I don’t have references handy but his website seems like a starting place: https://pit-claudel.fr/clement/ As I remember it, he was formalising compi
42.
by black_knight 2mo ago
There are approaches to GUI which are closer to formal specification than what is currently in use. Look at HotDrink for instance: https://tt.utu.fi/soft/hotdrink-gui-programming-with-dataflo...
43.
by black_knight 2mo ago
If I walked outside, I would also be an external tool. So, I don't.
44.
by black_knight 2mo ago
Agda. Fable and Opus both know it quite well now. They need some guidance to create good-looking code, but man, they know how to grind!
45.
by black_knight 2mo ago
It is a normalisation procedure for inductive and coinductive data types. Basically, the code is a function which takes in an expression where you can use generic data structures as variables and then some specific data structures, and it p
46.
by black_knight 2mo ago
This is a very insightful comment. I will add: The model is often completely implicit in the code. Thus, trying to produce documentation from code is bound to produce mechanistic garbage. I see two ways out. Either document the model separa
47.
by black_knight 2mo ago
I just finished waiting almost four hours for Fable to write 700 lines of code, based on my three paragraph prompt. Some speed on these harder tasks would definitely be welcome! It also spent almost 800k tokens on these lines…
48.
by black_knight 2mo ago
I miss modernism!
49.
by black_knight 2mo ago
GEB is not a difficult read. It is delightful! It is a popular science book which catches the vibe of mathematical logic in an excellent way. It is not a textbook, nor a piece of research. It's all vibes, but high-quality vibes. If you
50.
by black_knight 2mo ago
I showed up to first day at university and an older student talked to me for like two minutes before declaring that I needed to read GEB. I dutifully went ahead and bought it, and I still work in logic today.
51.
by black_knight 2mo ago
Not sure how true this restrictions is once you have the agents hammering on at a big code base of formalised proofs. Proofs stretching thousands of pages are split into lemmas, grouped into sub theories. What I haven’t seen agents do yet i
52.
by black_knight 2mo ago
I keep hearing that. At the same time people makes comments like the one you just answered to, using that analogy heavily. Could someone who understands both say where the analogy breaks down in this case?
53.
by black_knight 2mo ago
Same in Norway. I have been on the list for decades, and I never receive any unwanted calls – except from my mother (j.k love you mum!) I am not sure why it works so well here. I have vague recollections of news articles about it being igno
54.
by black_knight 2mo ago
Yes, one of the things I find hardest about using Claude code for Mathematics is keeping negativity out of the notes and memory. First of all, it will convince itself that a task is just too hard and find excuses not to try hard enough. The
55.
by black_knight 2mo ago
You are most certainly correct about this! And at the same time, I kind of cherish my ignorance on the proper ways of Nix. I have so many aspects of life where I practice perfectionism, and if Nix becomes another one of them, I shall have n
56.
by black_knight 2mo ago
I know nothing about the organisation of NixOS, but I know that NixOS is in a unique position now that LLMs have arrived. It offers the unique experience where you can fearlessly let the LLM loose on your system config to setup any convenie
57.
by black_knight 2mo ago
At the end of brev paper there is a section on the LLM usage. Now, this paper will undergo peer review. And thus, when published, we will trust the result as well as any other published result in mathematics. However, while humans are not i
58.
by black_knight 2mo ago
Lots of people talk about cheating here. That is not the framing I put in my mind. Or rather, if the students are cheating anyone it's themselves. LLMs exist and are extremely useful in academia. I am currently riding a productivity wa
59.
by black_knight 2mo ago
This article was the first time I saw that variation of the interrobang with the ! and ? angled and sharing the dot, but… man… I think I am in love‽
60.
by black_knight 2mo ago
If the proofs are formally verified by a proof assistant (Agda, Roq, Lean, ⋯), I see no reason we would need to know how these came about. All the information needed is in the proof.

More ›