"utter" meaning writing in the code, and "transfer" as in pass between functions/objects/processes/machines.
743 karma · joined December 9, 2014
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.
I hope they keep making it smarter! (Cheaper would be nice too, but smarter is my priority!)
I find Fable 5 still lacking in library design. But I guess there is no accounting for taste…
Agda is the most mature dependently typed programming languae (having been around since the 90s – it is basically Haskell on steroids), but has a more proof-assistant flavor than an actual programming language flavor. Opus & Fable write Agda quite well, so LLMs can understand dependent types.
I have several similar folders with variants of a construction, but taking differently structured input. They are named “plain”, “fibred” and “indexed”. So the fibred variant is clear enough.
The Claude speak I struggle with is “the capstone” and what name it could be talking about. And what folding means here. I think it just means:
“I changed an important result of the construction in the fibred variant, but kept the name. so the fibred variant is now different from the others.”
As far as I can tell "the capstone" is what Claude usually calls my current goal if it thinks it is a satisfying result.
"The fibred side folded its capstone into the existing name, so the kinds are asymmetric."
What on earth does it mean to fold a capstone into a name‽
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 brittle, non-functional mess that only in the most tenuous way resembles what I had in mind.
The job was never to type the code out. The job was always to take a problem in the real world, and shape it into a model which can be implemented in software. What LLMs do not do is to architect a system of suitable complexity to the scope of the problem. If you give a low skill worker the job of writing the prompts you will first get a prototype. Then a prototype with more features tacked on. Then a prototype with so many features tacked on that it breaks under its own weight.
Software engineers know system design, and can adapt the system design to the scope of the problem. Are we creating a single piece which will eventually expand into a big system, we need to design completely differently from if we are creating a robust stand-alone thing, which just needs to do one thing and do that one thing really well.
If anything, we will need stricter skill requirements for software engineers. Just because anyone can produce code which runs now, does not mean we should let anyone loose on creating the critical software infrastructure of our society.
A few different reasons why use an LLM when mathematics is done for its own sake:
Formally verifying my proofs catches any mistakes I make, but verifying is also hard work. LLMs shaves off a lot of time when formally verifying a proof.
I can still read through an LLM generated proof and understand it. This is a way for me to understand the result I am working on (usually in order to know what to prove next, results are not proven in a vacuum).
My experience thus far is that, while correct, an LLM generated proof is often unnecessarily complicated or inelegant. I take pleasure in elegant proofs and will spend time iterating on the first proof until I find it conveys the idea in the most elegant way. Having the initial LLM proof to start with is really useful, but is thus far rarely the final product.
The fact that it its own language does not preclude using it within the context of a different language. You can embed a domain specific language into a general purpose one.
Lets me ignore the LICENSE.md file, and use how I want.
https://pit-claudel.fr/clement/
As I remember it, he was formalising compilation by connecting the semantics of the higher level to the lower level one inside the proof assistant, so that proofs would carry through.
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 plugs them in for the variables. It then computes the structure of the resulting data type.
So, admittedly not a trivial task – hence the choice of Fable as the model. Also, this would have taken me few days to do by hand! So, we are living in the future! But one could always wish for more speed and more intelligence.