Możesz dodawać lokalizację do Twoich Tweetów, jak miasto czy konkretne miejsce, z sieci lub innych aplikacji. W każdej chwili możesz usunąć historię lokalizacji swoich Tweetów. Dowiedz się więcej
Putting this here for the next time "someone" asks the misguided question "why don't you use formal methods to develop Linux": https://web.archive.org/web/20140630071239/http://www.cypherpunks.to/~peter/04_verif_techniques.pdf … Personally, I like to think we have learned from past mistakes...
Ok, before everyone gets upset, yes FM can work in some cases, and provide great benefits, like the memory model work happening in the kernel. But look at that work in detail first before thinking about why it would, or not, work elsewhere.
Hint, remember, we don't really know how the CPUs underneath our code really work... :)
See, proving *everything* is expensive as hell (case in point: seL4 with 7500 LOC of code and 200000 LOC of proofs). But the thing is you *don't have to prove everything*; proving crucial code and/or logic is almost as beneficial: the way Wireguard or Firefox did it
sle4's "proof" went out the window when Spectre was announced. Which goes back to my original point, if you do not know how the hardware really works, formal proofs do not work. And none of us know how the hardware really works.
Twitter jest przeciążony lub wystąpił chwilowy problem. Spróbuj ponownie lub sprawdź status Twittera, aby uzyskać więcej informacji.
