black_knight
Even critical remarks are in the spirit of "You should do this better!", never the kind of gate-keeping bullshit I have seen in other fields.
It usually takes me two or three iterations to get there though. Discussing design and principles before writing the bulk of the code is a must. And then a pass or two of review to weed out ugliness.
Still saves time compared to writing the code by hand. Especially for tricky things, where type checking and tests can verify correctness.
For instance, in Sweden, to cherrypick a stat, in 1875 only 1% of military recruits were found unable to read [1].
We really must stop thinking that people of yestertimes where so much inferior to people today. Yes, there were differences between men and women, but this was also starting to change.
[1]: https://history.state.gov/historicaldocuments/frus1876/d308
But the 50% I do take into account, improves the text! And, like TFA, I never ask it for concrete text. It only helps me diagnose the issues, I prescribe the medicine!
False, at least from an American or Northern European perspective.
In the 1800s reading was an extremely popular activity. Not something restricted to a few. Printing press had been around for ages and the majority of the population read.
This situation suits me fine, since I am anyways more of an ideas person, than a crunching open problems person. But I understand the desperation of my colleagues who mad solving hard problems their identity.
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 orders of magnitude more intelligent AI can’t solve it even.
If it is impossible to prove, it might be possible to prove that it is impossible to prove, or that itself might be difficult or impossible…
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 remembering to remove old worktrees and prune the old branches
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 – the lingua Franca of IO.
Oh, want to use that other machine as a gateway? Just mount its /net.
Oh, want to route audio through another machine? Just mount their soundcard into your /dev.
Oh, your machine is too puny to do the task at hand? Just run “cpu thebigmachine” which transplanted your entire environment over there (all the virtual file systems) so that you can continue doing what you were doing, but using that machine’s CPU and memory.
This solved the problem of having to transplant your setup to the remote machine, which you have with modern SSH. If you wanted a different environment you instead created it locally. Each process har its own virtual file tree with mounts.
There were cool things at the local level too: All the programs would expose virtual file systems to interact with. Text editor? Each window had a directory with files containing window content, current selection, even the UI “tagline” with commands. This meant you could write scripts for your programs in any language, because you just had to interact with files.
A modern take on plan 9 is definitely on my Christmas wishlist!
I have used Fable for formalisation and it will, unless I catch it, reprove results it previously had proven, inline, in other results.
My experience is that it takes a lot of human input to make Fable write code nice enough for a formalisation library others can work on. But since this is certainly a lot of prerequisites formalised as well, it would be nice if not all of the effort was wasted on one capstone proof! (Repost of a earlier comment, but I feel it fits better here)
My experience is that it takes a lot of human input to make Fable write code nice enough for a formalisation library others can work on. But since this is certainly a lot of prerequisites formalised as well, it would be nice if not all of the effort was wasted on one capstone proof!
But the point is, you would not grant access to a “path” or some such. You gain access to a collection of actions, described by types. It can be simple “get/set property” or more complicated actions, maybe involving capabilities to several things at once.
To mint such an access token the “admin” will have say how the actions are performed, and then pass the token to you. The client code then will have a typed set of actions it can perform using the token.
This does not mean that we compile in the specific rights of each user or anything, it only means that we must ensure a valid flow of rights in order for the whole program to compile. You can get a capability in two ways: you mint a capability for something you already can do (you are the admin and own the data base, say), or you receive it (via an API call, say).
There is definitely a knack to design the system with this kind of flow. But once in place it feels very natural, you get the right to do something just in time for your need to do it. Very much principle of least privilege taken to an extreme.
The keys were there to stop an attacker, the type-checker helps the good guys stay in line.
A central authority is not a requirement. What is required is some way making sure capabilities are unforgeable.
This can be a central authority, which then has a completely mechanical task of registering capabilities and their ownership. But it can also be ensured “cryptographically” with a key.
The OS already has a capability system called “file descriptors”. Which works quite well, within its limited scope. This could be expanded out to more areas.
So, “utter” there means make a valid request with a key. On both the client side and the server side the keys and validations were invisible to the business logic, they just carried objects as usual.
You created capabilities by registering a handler for the operation, and got back a token object you could hand out and even send over the api to those who were meant to use them. And the clients got these objects which they could just manipulate and keep around for making API requests.
The cool part was that you could never forget to do an authorisation check. The keys were automatically checked when the request came in. An API request handler would have no privilege itself, it would only call the key-validated handlers created when the capability was minted.
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.
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 all your files by default then politely ask you which file it should read/write to? It would make more sense if the file picker was something the operating system ran when a program wants to edit a file, and what came back to the program after you selected was the accessor for that file (with read and/or write verbs).
So the program only have access to those files you have it access to. It cannot even ask the question to open another file, because it only has opaque accessors to those files it has been given.
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 transfer of nouns and verbs to perform the utterances.