You take hardware properties as axioms (for instance, ARMv6 cache coherency is specified in detail as part of the lengthy spec, even though you have no guarantees that the hardware actually is faithful to the spec)
Sadly, as ideal as this seems, Lean has a history of kernel bugs that allow one to prove False.
It's unlikely to be the case here as instead of hillclimbing a Lean proof for validity it appears the proof was first constructed in English before being translated to Lean, which intuitively (hopefully) reduces the chance it exploits a bug.
Looks like some of these place names have been overpowered in search results by their named-for sofa counterparts! When searching Finnala, Sweden, I essentially only get search results for the sofa, and even the Google AI overview, while admitting it's a locality in Sweden, shows me a picture of the sofa!
Mapping parts of files into executable memory, and then executing them, had better be bulletproof! Exploiting this seems like a direct path to RCE, and it's likely that this sort of library is used by privileged code.
Purely academically, this is a very cool piece of code! Just hoping that it gets a thorough vetting before used by privileged/security-critical software :)
Well, ld.so already does this, and it's no big deal. The Python interpreter also does this when executing a .py script (code is code, whether it's machine-readable or human-readable).
In any case, we take testing very seriously—every glibc shim we've written is covered with tests, and we run our loader against 1000 of the most popular Debian packages. The project has 100% code coverage. Perhaps, if I have the time, I'll also do some fuzzing on this thing.
Arguably the lower level abstractions are more interesting too! how exactly Windows does ring-0 is less interesting than writing your own ring-0! And unless you care about writing driver-level software for Windows or contributing to the kernel, learning this is also less useful.
I'm essentially arguing that unless you work at MSFT, there's next to no reason to learn that specific abstraction layer.
> I'm essentially arguing that unless you work at MSFT, there's next to no reason to learn that specific abstraction layer.
Really? Understanding the cost of ring transitions is incredibly useful. I recently consulted with a company that was having horrible performance issues, and it came down to the fact that the primary developer didn't know that certain Win32 calls forced ring transitions. The entire fix was switching from a mutex to a critical section (one causes a ring transition, the other doesn't).
Treating the OS like an impenetrable black box will bite upcoming engineers/companies... eventually.
To stream dns changes from site owners to dns servers. If you want to change a record, you post the change on atproto. DNS servers everywhere just subscribe to the jetstream. That way anyone can run a fast, local dns server which is kept up to date automatically.
I'd like to see DNS ownership combined with the time range and an owner-unique key so you can go to the website you intended to visit rather than whoever happens to own the domain at the moment.
Domains cost money to maintain. They can lapse, change, or be sold. Sometimes people make mistakes. So to my way of thinking they're great as a short-term named identifier but not as a long-term stable identifier. Would be nice to have both.
