arjvik

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)

was linked in the article!

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.

2 business days is a lot more strict than credit cards, which at the very least would not blink an eye at 2 weeks.

This is not exactly perfectly fair - appears that the first player wins 11/27 times and the other two win 8/27 each.

This makes sense, and I guess as someone who’s never written Windows software I didn’t realize it was a leaky abstraction!

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 :)

> Sofas → Swedish place names

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!

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.

Shortest-Path (Djikstra's) is in P :)

Sadly doesn't look turing complete (yet) :(

The way I've learned to read it is

    int v;

means that `v` is an `int`.

    int *w;

means that `*w` is an `int`, meaning `w` is a pointer to an `int`.

    int *y[5]

(note that `◌[]` has higher precedence than `*◌`, so this is `*(y[5])`) means that `*y[5]` is an `int`, so `y[5]` is a pointer to an `int`, meaning `y` is an array of `int` pointers.

    int (*(*kitchensink[5])(int, int))[6];

means that `(*(*kitchensink[5])(int, int))[6]` is an int, so

- `*(*kitchensink[5])(int, int)` is an array of `int`.

- `(*kitchensink[5])(int, int)` is a pointer to array of `int`.

- `kitchensink[5]` is a function pointer to a function that takes `(int, int)` and returns a pointer to an array of `int`.

- `kitchensink` is an array of function pointers to functions that take `(int, int)` and return a pointer to an array of `int`.

On your side here!

The clutch (and the potential to money shift your transmission) is _fun_, but not the reason that I want a stick shift - when pushing a car beyond normal limits just having control of when it shifts is enough. That being said, the up/down gate is just no fun! Plus, it lacks any feedback on what gear you're in.

understand?

It's really easy to understand that everything is typed as Any/Object/whatever upper bound type your statically-typed language of choice uses.

Desiring something better does not mean a lack of understanding of the status quo.