skysight-inc/HackerNews huggingface dataset:
>Bluntly, as long as gun control ultimately relies on use of force to succeed

And gun rights don't?

I have yet to hear a gun control advocate threaten violence, even implicitly as you have with the Ceaușescu, in the face of opposition to their political views. Meanwhile the pro-gun side threatens to kill their political opponents en masse in some nebulous future unless they are acquiesced to on a regular basis.

Between those two, which is really the one cloaked in authoritarianism?
Cloud can provider unlimited resources.

Maybe in future ,we will not need to make choice but choose the familiar one and totally relay the cloud’api and optimization.
“Branding” and “designer preferences” are bullshit that was specifically rejected by the design of the web in favor of information architecture and interoperability. Leave that shit in PDFs where it belongs and don’t bring it to web pages or native applications.
pfSense is still a great product in 2022? I had heard otherwise.
That is a very clear and helpful message.

You may want to consider mentioning it in the README.md as well and alongside any example/default configuration you generate indicating the default state and setting to disable it, especially if it's only output the first time it writes the telemetry history.
I think this sharply discounts the value of the step before the proof which is writing the specification in a formal language/logic. This often surfaces these misunderstandings before a proof is even necessary.

That doesn’t guarantee that the spec will be the right one (as you say) but it’s astounding how often just writing it down formally improves the implementation through rigorous thought.
looks fine...?
Personally, I think orphans are bad typography and have little to do with pixel perfection. I don’t see why responsive web design necessarily requires bad typography.

Given the tools to address these issues, such as Adobes proposed `text-wrap: balance`, I am sure many would do so.
In AU, mine doesn't turn off either.
It's my right to yell at anyone who accidentally steps off the sidewalk into my yard, but that right doesn't invalidate criticism and judgments I receive in response to my actions.
Good info thank you! Yeah I’ve noticed some weird stripping behavior in some clients like iMessage and Slack. Not sure if it’s the encoding or the length of the string that is my current issue but they both seem to play a role.
I wish browsers chose better default fonts which would make monospace, sans-serif, and serif more appealing. As an alternative, adopting new CSS keywords like user-monospace, user-sans-serif, user-serif could allow web developers to prioritize user-configured fonts in the browser.
I don't see the source for anytype on their github org, but I do see forks of various go libraries: ipfs, libp2p (protocol layer abstracted from ipfs), badger (a kv store), mongo, goldmark (markdown parser), amplitude (product analytics... "privacy-first"?!), etc. This doesn't mean that these libraries will definitely be used but it seems to paint a clearer picture of what it will be than the marketing team's meaningless self-flagellation that is the overdone homepage.
I am sure we can do better than predicate logic or types, but the code needs to change also. Code should be more abstract and reusable. If possible, it should be a subset of the logic. There is no point in verifying the same stuff in JavaScript, Java, Rust, Swift, ...

Furthermore, something that looks simple might need a lot of abstraction to become provable. Something might be simple to write down in code, but in order to come up with a notion of correctness for it, and actually prove it, might require something significantly more complicated.

Infatuation with Hoare-Logic is part of the problem (that's what the paper you link uses, I think?). Thinking that verifying programs is easier than doing proper math on the computer is a dead end. First get mathematicians to actually like doing proofs with the help of a computer. THEN you might have a chance of tackling more practical applications like program verification without using an insane amount of resources.
Oh nice yeah, seen a handful of very similar projects posted. This one you shared has a rich editor experience! I like that - thank you for sharing.
Happy to see another Talking Heads (TH) fanatic.

Pull Up The Roots has been the most impactful TH song for me so far. I was obsessed with it for about 6 months. I literally listened to it probably 2-3 times a day for those 6 months. I was in a point of my life where I felt like I needed radical change so "pull up the roots" was a powerful message for me. Also I love how weird and chaotic the message is and the song is just downright catchy to me.

https://www.youtube.com/watch?v=tQS6XfuH2wE

That whole Speaking In Tongues album is quite good. Definitely my favorite TH album. Great name for an album and very attractive cover art.

True Stories is also a very fun peak into the 80s. https://en.wikipedia.org/wiki/True_Stories_(film)
The truth about social media and anxiety
Robotic buoys developed to keep Atlantic right whales safe
I really want to like this, but it really comes across as more of a wishful thinking project without a lot of experience or intuition about how to solve the very real problems that formal methods run into in this domain. Like, the design goals literally include "verify any program" [1], which is almost certainly impossible.

Important questions like how you implement the design pillars without running smack into the issue of decidability seem entirely ignored. They have a whole section on how "this idea exists in an incentive no man's land" without seemingly being aware of the rich history of formal methods in low level programming, from Ada through Java through formal C through Rust itself. The common issues these encountered like decidability, holes in the formal model (which contributed to the downfall of the Java sandbox as a security boundary), and the combinatorial explosion inherent in verification tools are all huge looming questions that should at least be mentioned.

Maybe I'm being overly critical here and partial improvements are still improvements, but it'd be nice to see more moderate claims from authors tackling such an ambitious project.

[1] https://github.com/magmide/magmide/blob/main/posts/design-of...
Is the revenue $110/month internationally, or is that just the US rate?
> it would seem natural to find more heavy stars there that haven't burned out

Is that right? I thought the really, really big stars in the early universe burned-out in as little as a few million years.
Giving so-called designers a bunch of tools to make every web page behave differently and taking the design choices away from browser and platform vendors absolutely was a mistake and you can see it really clearly when you look at application design in the mid-1980s to mid-1990s versus the mid-1990s to now “designers get to do whatever they want” era of suck.
Are their any other large batch "donation" terminals besides those sent to Ukraine?
the terminals in AU, NZ, CA are all billed in local currency at a higher price but the currency conversion works out to approx. $110 USD/mo same as the US domestic terminals.
For reference, this is also the same case for AWS: https://aws.amazon.com/compliance/services-in-scope/

AWS US East-West (Northern Virginia, Ohio, Oregon, Northern California) is FedRAMP compliant at moderate impact level.
Formal verification predates Rust by decades. The addition of lifetimes and the borrow checker are worthwhile contributions to the field of provably-safe software, but there are a lot of other soundness properties that Rust doesn’t check (though people are working on it).
Um, isn't that kind of their whole thing?
GPU manufacturers have been talking about splitting the GPU market with products that are locked into only serving specific use cases like PC gaming, machine learning and cryptocurrency mining.

That's to say manufacturers want to prevent someone who buys a gaming GPU from using it to mine crypto or for ML, and they don't want someone who buys a ML GPU to use it for mining, and so on.
This was not about players. It's about the implementation.

I also don't know what you mean by "games are single threaded and feel very turn based". Games are usually not single threaded (insofar as most games run on multiple OS threads). If you want to say they feel single threaded, then it might be because the screen emits one frame after another, and you can influence the next frame by your action? But I don't know how that is an interesting insight and it doesn't seem to have anything to do with how games stay in sync.

You might have something interesting to say, but I wasn't able to learn anything from your post. Add to that the slightly accusing tone of it ("again conflating") I can't help but be annoyed.
CDC warns of 'Covid-19 rebound' after taking Paxlovid antiviral pills
There are too many scams in higher education
I am not convinced they treat their drivers worse than medallion taxi companies. In fact, I’m about 95% sure the reverse is true.
Rape victims would vehemently disagree.
That’s a great idea! I’m gonna try working that in. Thank you for checking it out.
Is this the end of Davos man?
@anibrowl, thanks, I’ve noticed FAQ a bit later.
It will be good if guidelines https://news.ycombinator.com/newsguidelines.html will have a link to https://news.ycombinator.com/newsfaq.html.

Also the error messages should be self-explainatory, at least has reference to appropriate section of FAQ.
I searched for word “fast” and it wasn’t found. Is it related to delay or noprocrast settings?
I am extremely skeptical of that calculation because a Prius costs $30,000 or more now. Maybe operating cost but not fully loaded cost including something like a 48 to 60 month car loan.
Of course?

How else would they know which laws in which locales are most profitable to skirt.

I am sure AirBNB has one for the same reason.
And you're back to fighting against a strawman. Nobody fetishized anything, except for you.

Also, you have no idea what my positions are about zoning or land use or infrastructure, as I haven't mentioned them.
Even if all these "key indicators" were accurate, how do they are they indicative of a lack of "a counterculture?" This article might as well be titled, "14 warning signs of social decadence," "14 warning signs of corporate dominance," or whatever else. Making some claim and substantiating it with a list of arbitrary observations is not a coherent way to make an argument.

What is a counterculture? Isn't alt/indie music marginalized by definition? Why would the (dubious) assertion that joke telling has become dangerous be indicative of no counterculture? What's an example of a period/place with a vibrant counterculture? Can any of these "warning signs" be present in such a period/place?

What the author seems to be arguing is that pop culture has become boring and repetitive. For a more interesting take on why this might be the case, see Mark Fisher, Ghosts of My Past--he argues that a set of structural conditions (such as no cheap rent) has led to media industries recycling safe, nostalgic content.
Ask HN: Why the boom in formal proof languages?
It seems anecdotally that there's a boom in formal proof languages. The posts on HN usually link to someone's in-progress repo "this language will aim to prove..." as in they are unfinished.

I am guessing there's an awakening coming from functional languages that mathematical proofs can help with code verification. Do you have an explanation if this is a phenomenon, what benefits there are, examples, etc?
Maybe this is the Aussie in me, but the middle finger as an offensive gesture is so mild I'd be surprised if anyone with access to the wider internet would actually be shocked to see it - let alone a cartoon emoji of it.

It doesn't have anything to do with abandoning tradition and living the edgelord life; the middle finger is firmly up there with "crap" or "bugger" on the "people were using this in ads 15 years ago" end of the offensive spectrum.
And redis/memcached are like 1% of use cases for database.
I don't see how flexbox solves this problem. Just because you vertically center text, doesn't mean that the visible text is actually centered. It depends on the font.
Yes. I imagine solving Maxwell's equations for this geometrical arrangement of neodymium magnets and cable would clarify all too clearly why they have "lackluster USB 2.0 speeds".
Is that in fact is a major differentiator between lyft/uber driving and other jobs (I'm dubious), then it sounds like a major and useful advantage of the platform that is reasonably worth paying for, albeit also one that is fragile.
You mean like dict() in Python? What's the use case for this?
Just to be clear, a substantial amount of that "donation" was actually funded by the federal government's USAID. Full details of the agreement aren't public as of yet AFAIK but USAID covered shipping and paid Starlink millions for terminals and potentially service.
I think if you could make a dildo shooting gun you would most probably bypass this law and store 100s of them. Afterall everything is big in Texas. So why not big dildo bullets!
In the SPARK subset of Ada, the specifications and contracts live alongside your code in the same language, then you can prove that the specs are satisfied.

You can also leave out the contracts and just prove absence of behaviors like divide by zero, out-of-bounds array access and integer overflow. Proving that code meets the specification can be really difficult but proving absence of bad behavior is usually a straightforward endeavor.
Austin had that for a while when they went and banned Uber/Lyft. They were... ok? The issue ends up being that it's hard to be a one-city service that's mostly used by people who don't live in the city. If I arrive in a random city, the last thing I want to do to get to where I need to go is have to search for which app I need to install and give my CC info to in order to get a cab.

NYC used to have Juno, but it went bankrupt in 2019. I feel like if you can't run a single-city rideshare app in NYC, you're gonna have a hard time doing it anywhere else.
On my system I've manually updated the Noto Emoji font to get emoji 14 support because I'm not updating to Ubuntu 22.04 on my daily driver to get the new font support.

Emoji are often rendered using the system's font fallback mechanism. When one font doesn't have the glyph required, another font that does have the glyph gets picked. Most fonts don't have glyphs for non-western scripts; there are only a few fonts out there that cover most of the Unicode standard, often made up of several fonts combined.

You're not manually changing the font-face mid sentence, but when you use emoji the renderer is definitely switching fonts to one you didn't specify.
We'll have to agree to disagree on that one. Here is a 670-year history of interest rates:

https://www.visualcapitalist.com/the-history-of-interest-rat...

There is a separate book you can read that attempts to go back 2000 years. Interest rates have never been this low in recorded human history, and there's an obvious reason why. The point of interest rates is to compensate the lender for deferring consumption. In a world without government manipulation, it makes no logical sense for a lender to be willing to lend money and receive zero or even negative interest.

The US government is artificially keeping interest rates low because recessions have become politically untenable, and the wealthy have totally captured the mechanisms of government. The end result is monetary policy which inflates assets for the wealthy while impoverishing the poor and middle classes. Other countries have been forced to adopt the same policies to avoid their currencies appreciating.

Worse yet, government is implicitly and explicitly backstopping and even socializing industries owned by the wealthy through fiscal policy. This is where you get "green energy credits" and "privatizing space," both of which have served only to enrich a couple billionaires. It's the western version of Russian oligarchs.
I think that it is because of smart contracts. A bug in a smart contract is very expensive.
First off I don't want to under sell Japan, it is a pretty nice country and Tokyo is pretty clean. Sadly it's still a city with car pollution all cities have.

Unique to Japan is the pollen. After WW2 Japan was reforested in mass with a single variety of tree. Thus making the exact pollen release an annual torture test for anyone without air filters. My theory is everyone eventually gets pollen alergies, it's just a matter of time. My wife is affected during pollen season, and I've starting to notice myself become affected as well.

We do not stir fry, that's not a thing in Japanese cuisine. And our cooking is all IH so no gas particle. Yet even we will notice if the air purifiers are not running. We'll first notice our noises are a bit stuffy, and omly then check to find a kid has turned off the air purifier.

An upshot to low pollution is filters last ages.
Here's a compilation of the best expert research, arguing for and against PR.
https://www.rangevoting.org/PropRep

A. The research compares proportional (PR) methods to plurality voting, the worst single-winner voting method there is. But superior methods like score voting and approval voting roughly double the accuracy (i.e. group welfare) compared to plurality voting. So no, there's no research showing the superiority of PR to these methods.

B. Even in that limited comparison, of PR to plurality voting, the data still is actually not that clear. For instance, Canada uses plurality voting rather than PR, and is rated as one of the most high functioning democracies by The Economist. Meanwhile lots of proportional democracies are far worse than plurality countries. Compare proportional Brazil (and several other Latin countries) to non-proportional UK, Canada, and USA.
Skepticism of the bottom line will be short-lived. Consider the economics of starship + starlink 2.0:

No more second stage cost, cheap propellant, an order of magnitude more connectivity per satellite, way fewer ground links required.

When the laser line of sight distances surpass those of terrain-constrained cables, it might start making sense to host latency-dependent servers in orbit. At that point, starlink begins to resemble internet 2.0
I didn't change any setting related to this and it has always been there. Like I said, the default shortcut is Control-Space.

Here is a thread with a screenshot and some users saying that the popup not working might be related to having the shortcut mapped to do something else: https://discussions.apple.com/thread/3045492
I think the number I saw was either 3000 purchased by USAID and 2000 donated, or vice versa.
> web python community was around at the same time as the scientific community while the two were relatively unaware of each of other

I didn’t dispute this, please reread what I said again.

> It just makes it look like you were in the camp that was aware of the scientific stack and not the web stack.

No, actually I’m a web stack Python guy mainly, I just actually know my history.
Sam Bankman Fried would be among those most likely to be co-defendants in a trial.

But, what I said was it’s never been documented.

* Does he buy Tether at par or at a discount?

* Can he redeem when he wants, in any quantity, or do they have arrangements?

* Is he redeeming for dollars or in kind? Terms allow for latter

* Does he buy with dollars or with commercial paper?

I do not believe he has shown material which would let us answer any of these questions
Okay, I need a smart person to explain to me why magnets don’t destroy my technology anymore. I swear growing up I was told that even looking at a magnet would wipe my drives and turn my screen into rainbows. Now we’re sticking them to our phones and iPads and throwing them in our laptop bags…what happened? Was it all anti-magnetic propaganda?
I've only done a bit of formal verification but I'd estimate that writing that spec was 7-10x harder than writing the actual program and was more complicated than the code.

In the end I had lower confidence that the spec lacked bugs than the program. This was after expending a huge amount of effort on a pretty tiny program.

I dont think this was a tooling thing. I think it spoke to the fundamental limits of formal verification. I think it'll always remain kinda niche.
Why wouldn't it? The cost to SpaceX shouldn't be significantly different per location. Maybe competition would drive different prices in different areas?
For backwards compatibility, most likely. If sans-serif on a particular platform has been FontX for 25 years browser vendors probably don’t want to suddenly change it for all existing websites.
How is this diff than the CVE list?
OS should not be detectable. There is no need for a marketing agency to know what OS you are using.
Gosh the whole p2p situation always reminds me of https://xkcd.com/949/, even with webrtc being a thing, I just never could get it to work reliably for huge files, it's been far easier and faster to just run a quick http server, and forward a port.
we are building a similar tool https://ossinsight.io/ which saves nearly 45B events from GitHub and can let you get more powerful insights from the project, e.g here is the history insights for K8s https://api.ossinsight.io/share/1bdadc17-6d94-41fb-8bc4-d6dc..., enjoy it by yourself :-)
To put some numbers on their costs, one Soyuz launch is about $40-50 million. A falcon 9 is probably a bit more expensive - Soyuz rockets are extremely cheap despite not being reusable. If the launches are dedicated solely to Starlink and not sharing significant payload space, that is about $200 million in expenses for the year.

Assuming a 5 year working life before the satellites de-orbit, the satellites launched this year have $40 million of depreciation. Other satellites have likely been launched as well and are depreciating in orbit.

That suggests that Starlink needs about 2-4x the paying customer base as today (depending on working life of satellites and launch costs, etc.) to break even.

That's a lot better than I was expecting.

Edit - someone pointed out that the $44M figure was monthly, not annual. In that case, it might be profitable. Also, I am aware of all of the "reusable" arguments, but a SpaceX launch still retails for $67M, while a Soyuz launch is still a lot cheaper at retail. This includes the cost factors of re-usability. Most of the cost of a rocket launch is fuel, not the metal tube.
The payments to the drivers not including all those other ones hidden away in other promotions
> That's certainly possible. Someone who has tried every possible way to direct their agency inward without results can simply burn out and feel helpless to affect change. By process of elimination, they've shifted their locus of control outward.

That's a clear and concise summary of what I meant. What, in your experience would the solution to such a Catch-22 be? I'm sure most reasonable individuals would want meaningful and effective agency but denying the reality and pretending they have sufficient agency isn't helpful either.
> Many places have out of date documentation — you should correct or update that information as you go through your first few months.

Expecting the newest member to update the docs seems to be pretty common but has always struck me as pathological. The person with the worst understanding and least perspective is the one who's expected to teach it to others.
Nice. Bought some.

The air here is already really good (~10 reading) most of the time so I reckon I can run my filters much longer than Xiaomi thinks is appropriate.
The S3 integration looks interesting. Do you have GPUs though? I think that's the main appeal of colab and I didn't see it immediately on your site
With high temperature superconductors, mechanical strain is in fact now the limiting factor, at least for the magnets.