black_knight

5 ms·

1.
by black_knight 5d ago
This mirrors my understanding when I use Claude code for mathematics. I can have deep discussions with it and it can solve my hairy problems. But whenever we go off the beaten track into design new mathematics, it struggles to make conceptu
2.
by black_knight 5d ago
The thing about mathematics is that it can be arbitrarily hard, including impossible to prove a given theorem. I don’t know the details of RH, it might very well be solved soon, but it could also be impossible or just so difficult that even
3.
by black_knight 6d ago
I think my layout is similar to yours. What do your scripts do? My branches end up in a tree structure (no shit!), and I rebase and merge up stream as changes land. I guess it could be more automated, but the only tedious part is rememberin
4.
by black_knight 7d ago
Could you explain the connection you see a bit more? Part of the appeal of the Plan 9 approach was that you could use any program in your distributed environment, written in any language, because the abstraction layer was the file system –
5.
by black_knight 7d ago
Plan 9 had such a powerful model for networked systems using these virtual file systems, it sounds like a fairytale! Oh, want to use that other machine as a gateway? Just mount its /net. Oh, want to route audio through another machine?
6.
by black_knight 12d ago
Kevin might not care, but I care more about building the foundation for future proofs and human understanding than I do about this particular result.
7.
by black_knight 12d ago
Indeed, that strikes me as a fine example of capability inspired design. The mechanism used is passing file descriptors, and for some reason file descriptors is the most "capability based" part of the Linux kernel.
8.
by black_knight 12d ago
Oh, I am quite sure there are inefficiencies! Just that they are not entirely inefficiencies. I have used Fable for formalisation and it will, unless I catch it, reprove results it previously had proven, inline, in other results.
9.
by black_knight 12d ago
I wonder if any piece of the lean code is in a shape which means it could be contributed to one of the existing Lean libraries. My experience is that it takes a lot of human input to make Fable write code nice enough for a formalisation lib
10.
by black_knight 12d ago
I wonder if any piece of the lean code is in a shape which means it could be contributed to one of the Lean libraries. My experience is that it takes a lot of human input to make Fable write code nice enough for a formalisation library othe
11.
by black_knight 12d ago
A human can cite previous published results. I am sure a lot of this development was formalising the prerequisites.
12.
by black_knight 12d ago
"utter" meaning writing in the code, and "transfer" as in pass between functions/objects/processes/machines.
13.
by black_knight 12d ago
First, I am talking about the capability based HTTP APIs I have worked on here. Not some imagined operating system. I can see if I get around to your question in the other sub thread. But the point is, you would not grant access to a “path”
14.
by black_knight 12d ago
I would hate to argue over semantics. But in addition to the keys being checked automatically at run time, the type system ensured that, unless the capability had been revoked, illegal requests would not type-check at compile time. Which I
15.
by black_knight 12d ago
There a sort of “might makes right” principle here. If you can do it, you can mint a capability for it, which means you will perform the action when someone with that capability requests it. A central authority is not a requirement. What is
16.
by black_knight 12d ago
I have designed capability based HTTP APIs before, it took some work but the end result was ergonomic. Of course over the web the capabilities must be secured in some way. I opted for keys to prove that you can perform a given action. So, “
17.
by black_knight 12d ago
The point is to flip the burden of proof. Instead of an authorisation system trying to find a reason to give you permission, you have to carry the proof in the form of a “verb”. Which you use when you perform the action.
18.
by black_knight 13d ago
I chose those words here because they are not programming language specific. For the OOPers, I guess you can imagine I said “objects” and “methods”.
19.
by black_knight 13d ago
You seem to understand it just fine. Your accessor, dirB, should not contain the “upload files” verb, while your dirA accessor (noun) should. My favorite example is the home directory and the file picker. Why should a program have access to
20.
by black_knight 13d ago
> can this subject perform this action on this object? IMHO, the most elegant method to answer this question is capability based access control. If the subject can utter the action, then it can perform it. And then delegation is the tran
21.
by black_knight 15d ago
I haven’t yet had a week without spending my Max Fable allowance. For my work (formalised mathematics) Fable is my go to for hard(ish) tasks and problems – of which I have many! I hope they keep making it smarter! (Cheaper would be nice too
22.
by black_knight 15d ago
Fable has become my go to in Agda as well. It just crunches hard technical tasks! I find Fable 5 still lacking in library design. But I guess there is no accounting for taste…
23.
by black_knight 18d ago
According to Hofstadter, it is not the ants themselves we should say are conscious, but the anthill. And it might very well befriend the anteater eating its ants.
24.
by black_knight 20d ago
Sure! I have done my fair share of pretending Java and C++ support my functional style. But at the end of the day, you have better support for writing that style in a real functional programming language. And I wonder how well one can enfor
25.
by black_knight 20d ago
Definitely room for improvement on Haskell's standard library when it comes to the number-related type classes. Modern Haskell could do very well in this area with a good type-class redesign in this area. The issue I think is that this
26.
by black_knight 20d ago
Or Liquid Haskell.
27.
by black_knight 20d 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.
28.
by black_knight 20d 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
29.
by black_knight 20d 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
30.
by black_knight 20d 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

More ›