They say in the Lean Zulip thread that this is actually intentionally a "low quality" release (https://leanprover.zulipchat.com/#narrow/channel/583336-Auto...); the paper notes that the quality is "inferior to that of expert-written Lean code". Then again, "Our results suggest that formalizing the core textbook infrastructure of modern mathematics is within reach".
I'm not, but is it yet possible to use the Vision Pro as a window manager for macOS? I'd totally get one if it were possible to lay out ordinary macOS windows in space rather than being confined to the simulation of a single rectangular screen.
On macOS, it is ultimately the app developer who is responsible for persisting and using state for windows, such as size and position. Think several terminal sessions - the terminal app needs to be the one to determine if it is representing the same 'session' as before after a restart.
If you are talking about remote display in a 3D space, the application would need to understand how to track and reopen a window in a particular location, and also there would need to be policy on how say a resize on the Vision Pro relates to the native window size once the Vision Pro is turned off.
This puts a lot of responsibility in the app developer's hands, where it is most likely not going to be accepted. So I would expect the experience to be sub-par.
There could be interesting workarounds for full-screen windows, since there are already the concepts of multiple heterogenous displays and display resolution changes on macOS. So you might have a screen, but the 'full screen' button is replaced by one which breaks the window out. The challenge would be making these persistent across connections to the Mac in a way that apps work well by default without picking up odd heuristics.
Yeah this seems like an obvious thing that would make it a lot more useful. Sad that Apple is barely scratching the surface of what’s possible, and it’s too closed for third-party developers to attempt to do anything like that.
At least for now, no, it is not possible. I agree that what you describe is how it ought to work in an ideal world, but it would probably require some serious rethinking of macOS UI/UX in order to make it work. For instance, it is not obvious what’s the best way to transfer the dock and the menu bar to a screen-less environment.
A hybrid solution I would love to see would be to have the current virtual screen, but with the option of dragging individual windows out of the screen.
By the way, you might be interested in looking up “blameless post-mortems” and indeed the field of incident response more generally. Modern incident response practice is to treat failures of an individual to do something as problems with the system they were operating in, because humans aren’t designed to be consistent or perfect and therefore shouldn’t be pretended or assumed to be.
I think it's more that the requested information is prominently featured in the article, and indeed is the content of the only graphic in the article below the intro banner.
> So far, Mythos Preview has found what it estimates are 6,202 high- or critical-severity vulnerabilities in these projects (out of 23,019 in total, including those it estimates as medium- or low-severity).
> 1,752 of those high- or critical-rated vulnerabilities have now been carefully assessed by one of six independent security research firms, or in a small number of cases by ourselves. Of these, 90.6% (1,587) have proved to be valid true positives, and 62.4% (1,094) were confirmed as either high- or critical-severity. That means that even if Mythos Preview finds no further vulnerabilities, at our current post-triage true-positive rates, it’s on track to have surfaced nearly 3,900 high- or critical-severity vulnerabilities in open-source code
I think you may have read a different article from me. The thesis of the article is summarised at the end:
> But if someone claims that the trend toward [X] will never reach some particular scary level, then the burden is on them to explain either:
> If they’re not treating [X] as a black box, and claim to be modeling the dynamics explicitly, then what is their model? Have they calculated the obvious things…
> If they are treating [X] as a black box, why isn’t their default expectation based on Lindy’s Law?
Like, the whole point is that in real life we do actually know things about situations and can model them; we fall back to Lindy's law when we know nothing at all. Further, arguments have justification to deviate from Lindy only when they give specifics about the situation they're modelling.
They say in the Lean Zulip thread that this is actually intentionally a "low quality" release (https://leanprover.zulipchat.com/#narrow/channel/583336-Auto...); the paper notes that the quality is "inferior to that of expert-written Lean code". Then again, "Our results suggest that formalizing the core textbook infrastructure of modern mathematics is within reach".
reply