skysight-inc/HackerNews huggingface dataset:
In particular, one of the more important rules I made when using CBMC was to keep the search depth for each invocation as shallow as possible. If CBMC runs in less than five minutes, you're doing it right. If it takes more than that, then you're asking it to do too much.

This led to the creation of function contracts and shadow functions. When evaluating functions, we actually want any calls that it makes to go to shadow functions instead of real functions. When we write a function, we include a contract that includes anything it may return, any side-effects it may have, and any memory it may touch / allocate / initialize. We then write a twin function -- its shadow function -- that technically follows the same contract in the most simplified terms, randomly choosing whether to succeed or fail. From CBMC's perspective, it's equivalent enough for model checking. But, it removes additional stack depth or recursion.

A good example of this would be a shadow function for the POSIX read function. Its contract should verify that the descriptor it is passed is valid. It should also assert that the memory region it is passed is bounded by the size it is given. The shadow function picks a non-deterministic state based on how it should set errno and how it should return. This state follows the POSIX standard, but the underlying system calls don't matter. Likewise, depending on the return code, it should initialize a number of bytes in the read buffer with non-deterministic values.

I used this shadow read function to find a buffer overflow in networking code and also to find a DOS infinite loop error in a tagged binary file format reader we were using.

CBMC isn't perfect, but when coupled with a good linter and -Wall / -Werror / -Wpedantic, it is a very useful layer in a defense in depth strategy for safer software.
Yep. Essentially what Linus is saying is that he has got to have more time, more competence, more vigilance that he wants because the other side can't or won't. And it's a recurring problem.

Sometimes we want more control and can't get it. Frustrating. Sometimes senior people are sick and tired of control and want less. Frustrating!
I'm fairly certain "www.canon" resolved to Canon's website at some point (where "some point" is the introduction of domain, 2015), and was not just a hypothetical address:

- https://icannwiki.org/.canon

- https://domainnamewire.com/2010/03/17/canon-why-would-you-wa...
Wow. When you guys first launched this was my biggest concern. This is absolutely awesome, thank you team!
Without being an expert in these matters it could be that while the earnings were good they may have already been "priced in"[0], so if the earnings weren't quite as high as expected or particular areas of revenue have contracted unexpectedly[1] then it could cause the price to move downwards. It could also be a result of larger market fluctuations, as a lot of larger F100 companies have also gone down by a similar amount today[2]. Any one of these factors or a combination of them together is likely the cause of the stock price movement seen today.

[0] https://www.kotaksecurities.com/articles/it-is-priced-in-wha...

[1] https://finance.yahoo.com/news/alphabet-misses-expectations-...

[2] https://www.investors.com/market-trend/stock-market-today/do...
> Why are they working on something that goes weeks without checking in code?

I think it was a couple of days' worth of work, which they told me was nearly finished for a couple of weeks. All I was saying was there was no way for me to know whether that was the true or not. Unless they pushed the code, which they were always supposedly on the cusp of doing. On the last day before the holidays I was very explicit that they needed to push their code by the end of the day, which they said they would but didn't.

Perhaps I need to be more assertive about it, or insist they pushed it live while I watched or something. I do think I'd have found the situation easier if we had a face-to-face relationship, although that's not really what I was trying to argue.
SIMD-Based Decoding of Posting Lists (2014) [pdf]
> Same thing with drinking and other harmful things.

I'm not sure where you're from, but other burdensome things aren't looked at that way in Australia, nor in other public healthcare countries I've been to.

Drinking, low quality/high calorie food, Netflix, food delivery, extreme sports - all things that place pressure on healthcare - yet I've never seen someone approach somebody eating McDonalds and asking then to not do that for the good of society, as I have with smokers.
rr is so good. "Where was this variable written? Where did this value come from?" Set watchpoint, reverse-continue, and bam you arrive at where the write happened.
It really isn't 'miles' ahead of the competition. If anything it is way behind. For example, look at Varjo: https://varjo.com/products/xr-4/
Vulkan For Beginners Tutorial #1 [video]
There Are 3 Kinds of Resumes. But Top Recruiters Say They Want to See 'Number 3'
It would probably be a €500 Knippex adjustable torque wrench. Assuming a German would use a tool for anything except it's intended purpose.
The same in Australia, but the line keeps getting hoisted out (as the tax keeps going up, roughly $2 per cigarette currently).
A TLD is just a namespace. Think of it like subdomains such as blog.yoursite.com

com is a top level domain, yoursite.com is a domain, and blog.yoursite.com is a subdomain. All of these can have their own DNS records that resolve to things. Typically they don't unless it redirects to something like nic.tld or something.
No, only if your browser has the right private key.

Let's say User A goes to the Corgea site. Their browser generates an RSA keypair, and appends the _public key_ to the URL, which is supposed to be visible.

When User B accesses that URL, User B's device generates an RSA keypair, and encrypts their message using User A's public key and User B's private key.

User B's generated URL will now contain User B's public key and the aforementioned encrypted message. User A decrypts using User B's public key and User A's private key.

tl;dr: Each browser client generates a keypair, and their private key is never exposed. You only ever encrypt/decrypt with _your_ private key, and someone else's public key.
That doesn't include the army of contractors they have/had that were laid off.
Is that not sort of exactly the point?

People love the concept of pokemon and monster collection, and it hasn't really evolved beyond the same RPG formula in 20 years.

Nintendo has utterly failed to deliver different experiences in the franchise. There's clearly an appetite for it.

I don't think different genres mean a completely different target audience. Most gamers play multiple genres, and there's a massive overlap of fans of Pokemon and fans of Palworld in particular.
Clearly, those 8000 employees were producing -$10,000,000,000 per year.
The fact that the Vision Pro today mostly runs legacy iPad and web software in 2D rectangles kind of makes it feel like Windows/386 which most people just used to run text mode MS-DOS programs inside GUI windows.
I think they have proved that it's a incinerator at this point.
Microsoft clearly wants Apple to spearhead this viewpoint that platform owners can't be regulated by legislation. It's entirely logical for them.
Who said anything about geniuses prospering? It's about the world prospering as a byproduct of genius work. And from my POV there is already plenty of that given the dizzying pace at which tech is evolving.
glibc marks freed pages with MADV_FREE, and on Linux, an MADV_FREE page won't be unmapped immediately. It's possible to read a value of an MADV_FREE'd page, have Linux swap the page out, and then read it again and now observe a zero-init'd page. If malloc returns a new allocation to a freed page, it isn't written to by the allocator (which would prevent the page from being subsequently zeroed if it hasn't already done so), so it doesn't guarantee that the contents won't be randomly zeroed.

Whether or not this is a sane OS I leave an exercise to the reader, but it is nonetheless the property of a common OS.
Musk says the first human has received an implant from Neuralink
I think this happens every quarter.
Yes but property values near greenery and parks are theoretically higher, right? At least in some places. It could also be beneficial for water runoff management and flood resistance to have more trees
I grew up on a dairy farm in Wisconsin (and I knew plenty of crop farmers as well, of course), and frankly none of what you said is congruent with my own experience. As orenlindsey said, farmers are generally smart people who have to juggle many hats and work their asses off in order to scrape out a very modest living. "Genius" is probably stretching a bit, but they aren't stupid laggards who get by on the inheritance they got from their parents the way you imply.

> The downside, of course, is that you need to be born in to it. A tiny 100 acre farm's land is worth north of 1 million dollars, not to mention a ton of other startup costs. Land isn't for sale very often, as usually at least one child wants to take it up. I don't even know how you'd approach starting from scratch unless you were already rich.

This is just flat out false. My dad started our farm (90 acres) from scratch. He did it by working his ass off, often working two or three jobs, while living frugally and saving as much as he could for a down payment. Then he got a mortgage, just like most people do when they buy property. It's hard in the sense that saving money is always hard, but it's certainly not impossible and something where you can't pull it off without a helping hand from your parents.
I'd like to understand how this compares to something like XReal with better UX (I'm assuming the software for XReal isn't great, I've never tried it).
The whole cert regime is wrongheaded. Issuing certs is vulnerable to exploits, the methods are clunky and problematic, certs expire so quickly that stuff is breaking more often than security issues could ever come up, there's no consideration to private networks, we still don't have content integrity without encryption, content proxy caching is dead, CAs can do what they want (there's too many CAs, cert logs aren't required to be validated in real time, you can't force a CA not to do something shady under a government gag order, etc), and there's a fundamental conflict between the owner of a domain and the issuer of a cert and the owner of a cert and the owner of some IP space or DNS server records.

But because it's this giant behemoth involving multiple industries, technological components, and vested interests, it will never change, save to implement bandaid after bandaid after hack after kludge. Literally the only thing that changes it is when someone with enough power (a market-dominant browser) forces it and everyone has to comply, or face creating a total shit-show due to lack of conformance. And we're all hopelessly dependent on it so it's not like we can do anything about it. The security of the web is a Kafkaesque nightmare.
Not really. The vast majority of modern TVs are 43, 55 or 65 inch sizes. That's three sizes.
Well, if total average costs per employee for G would be very roughly 1 million, there you have it. I think it may be half of that if at all, but it impacts the increased revenue significantly in any case.
After hours trading is also usually more volatile than regular hours, check in the morning and see where $GOOG actually opens.
> 94% of these positions went to people of color, 6% to white applicants.

Well that's wrong for starters. It's a net figure which counts a white person retiring and a white person being hired as a no-op if you interpret it wrongly like he has done.

Between that and the demographics of the young people applying for non-degree jobs (which far outnumber the higher level jobs) probably explains most of the stat.
There could be other factors in play like the recent volatility in Netflix within the same sector, as well as the upcoming FOMC meeting tomorrow causing increased fear. Markets aren't always as accurate and efficient as some believe, and stock prices always become more volatile around earnings.
Iff you pay an annual $100 dev fee.

Yes I know you can technically do this without a paid dev account, but it's practically useless because it has to be re-done every 7 days.
The broken Russian reads more like an advertisement to buy the real thing. Until you have supplied that quote I had no idea, even though I saw this picture.
Is it mirrored as some HEVC video stream from the laptop, or are UI elements actually rendered on headset itself?
In time or money? You can cancel your gym membership and work on it an hour a day
Never thought I'd see CP24 on HN
AMD Reports Fourth Quarter and Full Year 2023 Financial Results
> Ensemble is currently "pre-alpha": it's really more of a demo at this point. There's a lot of things I need to work on and until then it is unlikely I will be taking any code contributions.... The code is definitely not designed for general-purpose use yet, so don't expect much of it :)
> Putting aside your arrogance for a moment

Let's put aside making and taking things personally, shall we? One way to do that is by sticking to the relevant facts, so here's a relevant fact: two of those three companies aren't Bay Area companies. All three of them aren't even San Francisco companies. I think that's relevant if we're talking about San Francisco.

> All things considered VC's and high salaries for workers willing to take on risk has generally been good for San Francisco

That's a matter of judgment. If, say, a SFUSD teacher makes a different judgment because she has to commute from Tracy, I'm not going to say she's wrong.

> Tech workers making a middle class living off of investment money shouldn't be demonized

Who has demonized them? I haven't. I haven't made a moral judgment about this at all. I'm just arguing that economic policy and conditions tend to lead to predictable outcomes, and if we want different outcomes we should choose different policies.
Paying participants is standard practice for user research. You're showing that you value their time. If you don't have ready access to the kinds of participants you looking for, in most metropolitan areas around the world there are market research films that can find suitable participants and help you decide what's appropriate to pay them. You want the incentive to be high enough that you're not missing out on great people, but not so high that they're only doing it for the money.
We've already seen --

1. Significant migration from CA and NY to TX, TN, FL, etc. People make this about D/R politics, but it's really more about housing. The Rent is Too Damn High.

2. Net migration between the US and Mexico has been in the direction of Mexico for a few years now. Probably Trumpist xenophobia played a role, but I suspect that mostly It's the Economy Stupid -- partly that costs in the US are high, and maybe also partly that opportunities in Mexico have improved.
Because having your thing supported by mainline Linux makes interoperability a breeze and saves a lot of maintainership effort. There's a lot of money behind it. Dealing with the quality gate keeper is a cost of doing business.
.gy (Guyana) may have some life (grun.gy, lethar.gy ?)
Rhyming AI-powered clock sometimes lies about the time, makes up words
Ex-Chief Security Officer of Discord Interview (Kathy Wang)
We do have blacklists integrated already, but it's hard to get accurate reports and it's still just playing whack-a-mole. Without KYC coupled with it, the cost of getting a new phone number and picking up where you left off is almost nothing.

Requiring more KYC for gift cards would help in theory, but I don't know how you would implement that in practice. I don't know that I've ever had a worker check my ID to pick something up when they're supposed to, and you would have to implement a whole government ID verification system just to use a gift card online? Then it also adds a whole 'nother issue trying to legally resell gift cards.

Neither of those seems easy nor a solution.
We had fake nudes back in the day but not full blown photorealistic videos depicting hardcore sex acts.

There's definitely a difference there.
I guess it comes down to what you value. Their software ecosystem is certainly the best, but hardware side they're now decidedly behind.

>whereas most of the copycats are just trying to undercut on price

Some of them, at the premium end its the other way round. Copy cats are fielding much better hardware...at a price premium. e.g. pi5 vs orange pi 5+

8gb max vs 32gb max

1gbe vs 2.5gbe

sd card vs native nvme

BCM2712 vs RK3588

pcie gen 2 vs pcie gen 3

16nm lith vs 8nm

That's not to hate on the rasp...but they're just not in as strong a position anymore as they were in early pi3/4 days where they were the only game in town and competitively priced to boot.
I will do this thing you say.
OMG this really brings back some memories. I totally forgot about that .tk iframe thing. Wasn't it in the late 90s?
I've used a rowing machine with a VR headset (I don't recall which model, it was a few years ago, but probably some Oculus).

It was fun for a few minutes but not really usable for serious exercise:

- It's heavy and annoying (and this apple product seems even bulkier and heavier). The cable situation is also not great, you need a lightweight cable and ceiling suspension to keep it out of the way, but this is solvable.

- Exercise means you get sweaty. Can't wipe your brow and you have a wet headset on your face.

- You can't see your body and maintain proper form. The VR environment itself is also distracting if you turn your head around to look at stuff moving there.

I much prefer just to have my phone or tablet in fixed place in front of me to watch youtube or some movie.
Consistently 1-10 percentage points down is not great.

Unrelated does anyone have an intuition on why home ownership is higher for 21 y/o than 24 in millenials/gens category?
I was confused as well, so I checked various European languages for what their word for billion is. I suspect they are french, using an abbreviation for milliard, the French word for billion.
You are correct, and 60 minutes did a good detailed overview of this recently: https://www.cbsnews.com/video/60minutes-2024-01-14/

They highlight how the rolling nature of long-term commercial leases means that banks can kind of kick this can down the road, but only so much, and high interest rates makes this incredibly difficult. With this one it really does feel like we've jumped out of the airplane without a parachute and a lot of us are just going "Hey, nice breeze".

I'm not the most optimistic sort, so I'd love to hear any thoughts on how this doesn't end in complete catastrophe. It just seems like something policy makers and market participants don't want to talk about too loudly because they're worried about spooking the market.
It's absolutely the same target audience: Pokemon fans. There's a lot of us out here that haven't played a Pokemon game since the early 2000's when we played the 3rd basically-the-same Pokemon game and gave up.

Frankly, I think Pokemon's adult sales are mostly nostalgia and that the gameplay or genre matters very little. Turn-based RPGs can be a lot of fun, but Pokemon doesn't seem to have notably changed since I played it as a kid. It also exists in a world of competition; Baldur's Gate 3 and Warhammer 40k: Rogue Trader are both turn-based RPG's. The Divinity series as well.
In the same vein as .tv there is the .fm (Federated States of Micronesia) for radio stations.

Also, .ws (Western Samoa), which was sold as "web site".
.cx was probably most famous for goatse.cx.

(For anyone who doesn't know -- don't go there. At least not while you're in public.)
You're talking about the US economy?

The "by any metric" statements seems false. A "not doing fine" does not have 54-year low unemployment rate @ 3.4% [1]

US GDP growth for since 2022 Q3 has been in the 5% range (very strong) [2]

Median individual income is at an all time high, poverty rate is at a 10 year low (2% decrease from 2014 to now, not huge percentage wise, but that is still 6 million people)

On the flip side - yes, home sales are at a low. Increased interest rates and a real estate market that saw a price correction in 2011 and 2020 with the corresponding economic recessions, has not made housing any more affordable at all.

> Tech CEOs don't control the interest rates. The interest rate effects their ability to get free and cheap money.

True, though that free & cheap money means more people can start companies, grow their companies faster - and that in turn creates bottom-up economics where more people have more disposable income and can then buy homes.

My second mortgage is now absurdly expensive.. But yeah, we are seeing the result of the Fed policy to try and _cool_ the economy as much as they can. One of the big levers they have - interest rates. The Fed intentionally made mortgages more expensive.

Further yet though, housing inventory is a big factor, which you then need to look at local governments and zoning restrictions for why there is not more housing built.

In sum, the wider economy IS doing fine by several metrics. Inflation AFAIK was not really a factor for home prices to increase. That was caused by the Fed, a a deep pandemic-induced recession, and all of the same forces that have caused housing prices to increase since essentially the 70s & 80s [4].

[1] https://www.commerce.gov/news/blog/2023/02/news-unemployment...

[2] https://www.bea.gov/news/2024/gross-domestic-product-fourth-...

[3] https://datacommons.org/place/country/USA?mprop=amount&popt=...

[4] https://fred.stlouisfed.org/series/MSPUS
Re: your edit

An experience not bogged down by "brand safety"
Something to be said for using mass-produced, very cheap, locally produced electronics in military stuff. Even moreso when the electronics engineers you hire stand a good chance of owning a few at home.
There’s plenty of reasons why you would want to have a separate Apple ID for a company Mac that have nothing to do with overly restrictive permissions from IT.

The main one being a complete separation of calls, messages, calendar, notes and reminders. For my own sake more than for my employers sake.

And many employees with company phones already have that separation. iPhone and Mac is not that uncommon to provide for employees. But an iPad on top? I think that’s gonna be much harder to find

And edit: a Vision Pro on top…
I would have said to just use dot-org once upon at time, but then this happened: https://www.eff.org/deeplinks/2020/12/how-we-saved-org-2020-...

In the meantime, at least thepiratebay.org is still up... and now that I think of it, it's a good canary for the integrity of dot-org.
> There's nothing special about farmers, they aren't geniuses, the work is not that difficult

This is absolutely laughable. The work is incredibly difficult. It literally destroys your body, every old farmer I've ever known has a heap of medical issues from having to do a lifetime of physical labor. It may not be intellectually difficult, but it's very difficult work.
Processor clock speeds are not how fast AIs think
Costs do not impact revenue only profits.
Nostr is not a payment network. You probably used Lightning instead.
Don't worry, he's talking out of his ass about farming as well.
Imagine if other engineers had this attitude towards tools: "I don't use a ruler when making a drawing. You have to reach a peace of mind to make a straight line and the junior nowadays just use a ruler instead. "

I say that as someone who programs on paper and uses print debugging a lot.
Not sure what kind of visa you applied for but an employer is liable for all visa-related fees

https://ogletree.com/insights-resources/blog-posts/u-s-emplo....
Working out with a VR headset on seems like a great way to get the whole thing disgusting. Hope I can put this $3500 face computer through the washing machine.