I listened to an interview with one of the researchers. They had a component to verify "this binary will never allocate mem outside it's allowed area" and by statically verifying that they could enable high performance IPC. Also, that was the source for the decision to allow it to run on Ring 0. That's what stuck in my mind.
Sounds a bit like Microsoft's Singularity project, though I don't know if they even used a proof system to ensure a program couldn't do bad stuff(TM). After verification they just let the program run in Ring 0 (kernel space) of the CPU to skip even the performance hit of the cpu's isolation.
> [int overflows, etc.] No runtime cost when Z3 can prove it. Otherwise, the compiler emits a safe runtime check as fallback.
Super interesting approach. I see this eventually be integrated into future mainstream languages, though that may take a while. I suspect that the game programming crowd will try to use it first, due to the possibility to prove certain edge cases at compile time and skip the runtime cost. But perhaps this optimization drive is no longer the case because we've got bazillions of cores nowadays. I may be too old for these predictions. Cool nonetheless.
Over the last year or so I arrived at a (sort of) MQTT semantic broker that facilitates an actor architecture. It supports federation (including transitive, so proxies "just work"(TM)), transparent outbound buffering with disk overflow and encryption with the noise protocol. Building apps on top of it is a joy. Rust.
edit: ah, yes also a broker controlled component manager that can start, stop, monitor services over the mentioned broker. This is the carpet that brings the room together.
In most of Germany neither is required (Baden Württemberg requires non-EU citizens to pay 1.5k€ per semester). Commonly though you have to pay from 200 to 300€ administrative fees.
The harder problem is to enter Germany, but as you have EU citizenship, that's not a problem for you.
I tried coding "ownership strictly" in Rust myself for a while and I've given up for the most part. In a lot of cases I painted myself into corners that I couldn't get out from without changing everything. That is probably a signal I should use, but Arc and clone also work. So I use them.
And you can spend your effort on features and architectural issues rather than smaller scope bugs. My experience is that Rust enables me to focus on features as long as I don't give the AI free reign. Architecture matters for correctness bugs, because some solutions are inherently more prone to the AI becoming confused along the way than others.
The more effort I spend on planning architecture with the AI, the less runtime bugs I need to investigate after it did the implementation.
Discovery of the best solution in a problem space is not generative but only verificative. Meaning: the LLM can see if a solution is better than another, but it can't generate the best one from the start. If you trust it, you'll get sub-par solutions.
This is definitely an agent problem instead of an LLM problem. Anybody got something explorative like this working?
For the love of god, don't do blank textiles anymore. In the end you have a software that has 20 (or more) individual files for each programs section, which works fine until you want the files to be consistent. Boom. And then you add a lock to fix it and suddenly your whole program can only run sequentially. And then your customers ask why it's so slow in ingress. I won't name any names here, but this is a real commercial product.