skysight-inc/HackerNews huggingface dataset:
Sure.

1. Dependent types, because they offer 100% certainty in the propositions they express (assuming they're proven) suffer from the same problem all sound verification methods suffer from, and that is fundamental computational complexity costs of verifying something with absolute certainty. I summarized some of them here: https://pron.github.io/posts/correctness-and-complexity (there are some properties that are easy to verify called inductive or compositional properties -- not surprisingly, the properties verified by simple type systems or Rust's borrow checker fall in that category -- but, unfortunately, most correctness properties aren't compositional).

2. Dependent types rely on deductive proofs for verification, and deductive proofs (the "proof theory" part of a logic) are the least scalable verification method as they are least amenable to automation. That's why model checkers (that provide proofs based on the "model theory" of the logic, hence the name model checkers) scale to larger programs/specifications. In addition, deductive proofs are much less forgiving of partial specifications. In other words, the contract (or type, in the case of dependent types) must express every property of the algorithm you rely on (unlike, say, concolic testing). This makes writing specifications very tedious. Unsurprisingly, deductive proofs are the least used formal verification technique in industry, and it's usually used when all other options have failed or to tie together results obtained from model checkers.

Those were the theoretical limitations. Here are the practical ones:

3. Unlike contracts, type systems tie the specification method (types) to the verification method (type-checking, i.e. deductive proofs). This means that everything specified with a dependent type must be deductively proven, or it has to be specified in some other way (i.e. you also need contracts), or else you risk making even your simple types unsound (although I hear some people are working on relaxing that problem, and that's what I mentioned in my previous comment). But properties differ greatly both in the confidence you need as well as the effort they require to achieve that confidence. Contracts give you the freedom to specify your program however you like, and then choose, for each property, which method you'd like to use to verify it -- deductive proofs, model checking, static analysis, concolic tests. randomized tests, manual tests or even inspection, all without risking the soundness of the type system, on which the compiler relies to generate correct machine code. In short: dependent types are inflexible in that they force you to use a particular verification method, and that verification method happens to be the least scalable, most tedious one.

4. Because dependent types are so tied to the program, the program must be written with the specific properties you want to verify in mind. If, after writing the program, you want to prove other properties about it, you'll probably need to rewrite it.
> If complexity is based on how likely a syntactically correct program is also logically correct, then type systems remove a lot of complexity.

Types are not really at the syntax level. I would measure the complexity of a language by the complexity of it's grammar and the size of the standard library/amount of common idioms needed to write most programs in a reasonable way.
Maybe for now, but everyone I know in my age group that was super into these (23-28) is currently trying to sell them because they have too many and the novelty wore off.

Feels basically like a Beanie Baby craze, except this time, the people who are into actual quality or give off the hobbyist vibe go to other products like Nendoroid.
1. Bidirectional typing can be easily generalized to dependent types. You can't always infer the type, but an 80% solution is definitely good enough for inference.

2. Your types don't have to be full specifications, and you can refine them later, no?

3. Idris, at least, doesn't force you to make all your functions total, and functions are actually partial by default.

4. Again, in Idris, implementations are hidden by default across modules. Maybe there's a nice middle-ground between hiding everything and exposing everything, but I don't know what that would look like.

5. What are the competing approaches and how are they better at dealing with, for example, distributed computing?

I'm not very familiar with dependent types, but none of these seem like fundamental restrictions.
Summer camps using facial-recognition tech to give 'a glimpse of life at camp'
Bukowski may have said, "If you're going to try, go all the way," but Bukowski's tombstone reads, "Don't try." Bukowski spent most of his life as non-functioning alcoholic, a lifestyle which is unenviable even in the slightly-romanticized form he presents in his writings. If you ever want to watch something truly unpleasant, pull up YouTube and watch him berate his wife on public television (possibly drunk). Bukowski was insightful on a lot of things, but his life doesn't look like a happy one to me, and I'd be cautious about taking life advice from him.
Greenland
Great episode of Peter Thiel and Eric Weinstein discussing this slowing of technological progress: https://www.youtube.com/watch?v=nM9f0W2KD5s
The edgy protesters are specifically targetting the government, the police who is acting on behalf of the government, and sometimes things associated with the CCP/PRC (e.g. PRC flag).

Some of their actions have caused trouble for others, but in general, they are not interested in pure destruction.

Of course there are exception cases, I'm speaking of the situation generally.
Employer May Be Spying on You and Wasting Its Time
You are correct that "face" isn't an idea that is unique to Asia. But on the other hand, if you don't think there is an extra emphasis on it in certain Asian cultures (can't speak for China, but I have lots of experience with Japan), you are simply wrong. The lengths Japanese people go to avoid bucking a trend, or staying within the cultural boundaries is, on average, much further than most Western cultures would.

For what its worth, I don't think this is a good or a bad thing. While it can certainly have its problems, I also think its a key ingredient in why many macro-scale societal issues in Japan (mega cities, public transportation, crime, etc.) simply seem to work better, more efficiently, and with less friction than Western counterparts (particularly the US).
I agree, was referring to the following more than the original tweet:

> Is there a list of gender-neutral insults that we can refer to for compliance reasons?

The thing is that even if there is a list like this now, in 9 years saying 'woman' might not even be acceptable because it has 'man' in it. If 'woman' isn't something we say in 9 years, I don't think twitter, in 9 years, should start banning everyone who every tweeted it now.
Is it really that great for the doomsday scenario? If a person is in the same room and Bluetooth works, I don't need any special app for sharing files. If it is remote, I don't see how spawning a wide area mesh network should be even possible with the most recent generation of smartphones. The sending power is just too small.
Am I the only person that believes international crime will see a significant drop if China controls HK?

I'm actually glad this glorified money laundering/financial crime haven is being shut down. The sooner China gets extradition powers, the sooner we can close the criminal enterprises operating in/through HK for the past 1-2 centuries.

Running drugs/drug money through HK is something that has been going on for a very long time (thanks to the UK/US/etc), time to put an end to it.

Lot of big money manipulating kids that can't see through the haze neo-colonialism.
Traditional Brokerages Are Being Disrupted
As long as you citing things you haven't actually read is considered good practice (hint: Turns out it is!).

I think it's probably harder to do this tech than you think; on the other hand, I am continually amazed at the acceptance of throwing whatever citations you haven't read that you want in, so the bar may be low.
Omitting html, head, and body tags is allowed by HTML specs, and the script tag's default type is "text/javascript". So it could be further simplified to:

<title>Test</title>
<div id="howdy"></div>
<script>
document.addEventListener('DOMContentLoaded',
() => document.getElementById('howdy').innerHTML = 'Hello world!'
)
</script>

Edit: formatting
Power Law Distribution in Network Science
Vue offers a more gradual learning curve coming from HTML. Because in the beginning, you don't write components in JS at all. Instead, you can use Vue "directives" like `v-if` right inside your HTML. Later, when you're ready for components, you have to add a compiler.

React takes a different approach. It doesn't "pretend" to be HTML by extending it with custom directives. Instead, it forces you to start the journey in JS land. That can be frustrating at first if you're unfamiliar with JS. But the gap between "simple" and "complex" is smaller: you learn the idea of components once, and can apply it with or without a toolchain.
Look at the reviews for Amazon's choice for "iphone charge audio". The questions, pictures and reviews are about some totally unrelated product. I'm not sure if Amazon sold this slot, or just randomly chose from a huge assortment of crap listings.

(Though seriously, if anyone has a recommendation of a decent product to charge an iPhone and allow audio out at the same time, please post it)
The New York Times Town Hall—The New York Times Unites vs. Twitter
See https://unix.stackexchange.com/a/294206/5132 .
This article is only considering static images. Lidar static "images" necessarily contain depth information so yeah obviously they'll have better depth estimates.

But that's really beside the point because the world is not static and any system attempting self-driving will need to take that into account.

Using parallax measurements which is what Tesla says they are doing, you can dramatically increase the estimates of depth measurements by comparing multiple frames of 2D images.

Also, just a reminder that Tesla is also using radar in conjunction with the cameras.
I think the western society is objectively further advanced than the Chinese one. Not surprising since China is a country in development and most other countries have gone through similar phases. So it should not be taken as a accusation. This conflict aside, I wouldn't see them on the same level.
Don't want to be pessimistic, but I guess all "high tech", especially customers "internet of things" and mobile devices, will be the first thing to become unusable bricks in the doomsday scenario. Better keep pen and paper at hand... Or at least a reliable printer and your old solid notebook ;-)
Putting aside the surrounding argument of whether Twitter is right to have this content policy, and accepting for the sake of argument that this is the kind of tweet that Twitter’s policy does censor (if haphazardly applied), I guess I don’t see the age of the tweet being necessarily relevant. All twitter content has long-tail reach, if Twitter has decided that they don’t want their service to ever have that content, then grandfathering old content doesn’t make much sense.

The question of whether the content flagging was automatic is an interesting one. In other instances, such as James Woods (who is still in Twitter purgatory) [0], the message he received doesn't have any language that indicates that it was manually reported and flagged, which it most certainly was.

Given how slow Twitter has been to roll out features in general, and Jack Dorsey's continued insistence on avoiding heavy handed moderation and policies, I have to doubt that Twitter rolled out an automated content system with such high potential of being an embarrassment. I don't know the author, but just because he isn't a frequent/recent Twitter user doesn't mean that an angry Internet mob from some other community hasn't decided to target his Internet accounts in general.

[0] https://twitter.com/Millerita/status/1119655394899415040?ref...
I was expecting X11 tools such as xev, xdotool, wmctrl, etc. Not a list a more or less obscure graphical programs (some stuff are even using GTK in the list). Fun nonetheless.
Hong Kong student leaders and their families face anonymous threats
Thanks for the feedback. I'm going to give it a try.
Don't forget to thank him for `avahi' too.

Avahi is a fun whack-a-mole game where your computer hides the network connection. You win the game by remembering to kill processes and setting up stuff manually, like most games produced by LP studios.

edit:
Other popular games include:

SystemD: hack your way through a blob of intractability. Try it on Nightmare mode, where you're only given access to a empty bootscreen, for a real challenge.

Pulseaudio: Experience the sound of no hands clapping, in a forest where trees are falling with no one there to witness it. Also, the forest is on fire!
who happened to singlehandedly convince more people to switch to BSD than anyone ever before him
how do you find the time - sorry for asking personal questions but do you work full time, what about kids stuff?
I try but unable to consistently commit more than 20 min on an off.
You get pretty decent support if you have Google One. My wife had an issue, clicked the support thing and was talking to somebody in a few minutes.
Yes, but rust can be seen as an alternative to C++. They are closest in terms of features/power/performance.
I use a standard PDF reader and then the ZotFile plugin. ZotFile processes highlighted text and comments made in PDF compliant ways and turns then into notes in Zotero.
Deleting the tweet would be like pretending they never said that in the first place, which is arguably worse.
As someone who worked in a similar section (animation), this is great news. Autodesk tools (especially Maya) are way too expensive in what they deliver. I'm glad many big studios realized this in that they either build their own tools (Pixar/Dreamworks) or they adapt Open Source (Blender) and help improving it.

There is still other tooling (Cinema4D, ZBrush) but those are actually working.. Maya has failed me so many times, I cannot recommend it in any way other than it is still (sadly) used very commonly among studios. And artists do not like to learn new toolings, that I also know from experience..
edit: grammar
It didn't work out all that great for them.
gotta love jwz. he is forever thankful by all the HN types that made him a millionaire and allowed him to live like an angst teenager forever, that he goes out of his way everytime to show it
You can move around the execution in the VS debugger - if you’re at a break point you can move execution earlier in that function etc. That’s the only debugger I’ve seen doing that though.
The GTK screenshots all use then ThinIce theme[1] – still my favorite, but sadly not available for GTK 3 or 4. And I guess it wouldn't fit with GNOME's current design direction anyway.

[1] http://thinice.sourceforge.net/
It is simply not produced. Methane is CH4. The carbon goes into CO2 instead (which is bad, but not as bad for the environment as methane).
In the UK at least, the people who've managed to bootstrap themselves to success through hard work and good decision making are the overwhelming minority.

The causal chain seems to roughly be: Top jobs tend to belong to those who attended top universities. => Top universities are attended by those who went to private schools. => Those who went to private school are either from wealthy families or attending on scholarship due largely to the fortune of genetics and/or an educated family. I certainly benefited from that (school scholarship => Oxbridge => good tech job), but I don't know that I could have if fortune hadn't smiled on me.

I agree that even with all those benefits, you can still fail if you make poor choices. However, I don't think the vast majority of people with worse circumstances can just choose their way out of it. It's not to say that it's impossible - my grandma has a rags to riches story that's only slightly marred by her similarly ethically dubious sales techniques...
Mimetic Traps – Brian Timer
https://docs.blender.org/api/current/
The fair choice is a text box: enter your search engine url. If you don’t know what it is, google it. The purpose of the legislation should be to make users aware of their options, not to let google prefill it for them. Users bear much of the responsibility for creating monopolies and have a duty to be educated about the market, if they wish to keep having a free market.

This would create an incentive for search engines to spend the money on ad campaigns for brand awareness instead of bidding for google. Win win for the market
I don't think it's broken, this is by design. The Justice System has always been a tool of capital to control the working class. This is an example of it doing what it was designed to do.
I’m a Gsuite, maps and YouTube user. I want to move away from Gsuite and maps but don’t think there are good alternatives.

CityMapper comes close but isn’t there.

FastMail support is worse than Google and has fewer features.
it's not obscure I'd guess
Adobe, back a decade ago, was quite liberal on that front - the stuff was easily crack-able, keygens whever one would look. As a result, whenever I ask colleagues with Photoshop skills how they acquired them, the answer always is "with 14 and a Photoshop crack".

Clever move to not stand in the way of cracks for amateurs too much until they introduced an affordable (!) subscription.
It’s not a simple, linear relationship. People generally do better with whole foods which have higher fiber content. That tends to make more gas. Gas is the result of gut bacteria digesting fiber. Certainly too much gas can be a symptom of poor health, but so can too little.
But this is how the Hong Kong government has traditionally made its money. Hong Kong’s tax structure is real-estate sales. This is why Hong Kong is all about huge sky rise developments of ultra-small apartments... and because the island is all hills, it is also why so many developments are built literally on a cliff.

Hong Kong is a geographically difficult place... building new plots is expensive - and the government makes it more expensive.
They're demonetized all across the political spectrum. Be it right wing like Crowder or left-wing like Tim Pool.
In other words: why GUI configuration systems should allow comments, just like text config files do.
Whips in the soul.
So whats the alternative? Do nothing at all?

If you have $100k left to pay on your mortgage, and somebody offers you $5k towards the mortgage are you going to tell them they're offering you a "false hope because you'd still have $95k left to pay"?

EDIT: This is also known as the "nirvana fallacy": because the solution is not perfect - that means it is worthless.

https://en.wikipedia.org/wiki/Nirvana_fallacy
Whereas an algorithm can be trusted to moderate ethically?

This is why civilized countries have developed rule of law, including arguments and rebuttals, overseen by an impartial arbiter.

Yes, that is costly. But it is the accepted solution we have as a society, and it's time "Big Tech" starts accepting rule of law.
Potential road capacity is far higher than is currently achieved by human drivers. Rational coordination and less accidents are more than feasible. Platooning is estimated to have the potential to increase per lane capacity by 500%.
No great technological stagnation (2016)
> The protesters learned in 2014 that having leaders was a weakness. Once the leadership was arrested, the heart went out of the occupy movement, and it lost momentum. So in 2019, there is no leadership at all.

Another thing that's similar with the (still ongoing) Yellow Vests in France.
The article doesn’t _exclude_ boys. ‘what about x?’ is just a language game.
Can't you both criticize Twitter and use open platforms? They aren't mutually exclusive.
Great news. Excited to try it out. Thanks a lot.
India's TFR is reported 2.2-2.3 for 2018. That is, for a developing country with high child mortality, the replacement rate.
That is a rather disgusting accusation to make, and one that eimultaneously indicates a political bias and presumes that automated moderation decisions are always correct.
Twitter uses third-party contractors for human moderation. If the tweet was reported/flagged and made its way into manual review for a human, whoever looked at it probably didn't take more than 30 seconds to decide. Even if Twitter's moderator workforce is U.S. based (and thus, attune to cultural norms), they probably are optimized to issue suspensions for low-hanging fruit. Vulgarity is going to be more of an obvious signal to the average person, than obfuscated hateful messages.
This seems to be the perfect example of extrapolating generalities from personal experience alone. I don't know if there is a cognitive bias that describes this, but if not, there really should be. The world is much more complex than your personal experiences. It is really tempting to believe the larger world matches what you experience, and I think that's the default state, but it's completely wrong.
“The Social Network” was the most important movie of all time
XRoach doesn't work even on a modern X desktop. The background window on, say, gnome, isn't really the root window. I compiled XRoach a few years ago and didn't understand at first why it wasn't working. I don't know if any of the modern desktops have an actual root window that's visible.
Support-Vector Machine
Anecdotally, taking in a little chlorophyll per day dramatically reduces how much gas I produce. So in my experience, it’s at least possible the effect may be large. Worthy of more research.
> Microsoft outright encourages this

But MS does not encourage you to sell access to those unlicensed copies. Corellium's business model isn't security research, it's taking illegal copies and "renting" them out to people for money. And people go to them because it's convenient, not because there is no other legal way.
heck yeah! "what can a technologist do about climate change" is my daily mantra.