skysight-inc/HackerNews huggingface dataset:
> It would be great if you've mentioned them and briefly described why are they limiting.

I've done so here: https://news.ycombinator.com/item?id=20714845

> Is extremely complex. Proving complex programs using constrain solving would be too expensive, if possible.

The same is true for deductive proofs, of which dependent types are a particular instance, only the problem is far worse. It is true that there are cases where deductive proofs are more feasible than model checking, but the converse is true in a much wider portion of cases. That's why deductive proofs are rarely the first choice, and they're used selectively, usually only after other methods have failed. Overall, deductive proof, although it certainly has its place in certain circumstances, is the least scalable verification method we have. This means that it's the last method you want to use by default, let alone bake it into your type system.

> Constraints are being accumulated (tho not linearly) when the program grow and so does its state.

This is true regardless of the verification method used. See my blog post here: https://pron.github.io/posts/correctness-and-complexity

> When you proved lemmas for a small block of code, you simply reuse those for higher order proofs.

No, you can't "simply" reuse results. Here's an example (given in the post in Java, my preferred language, but as this is a post about Haskell, let me show it in Haskell):

foo :: (Integer -> Bool) -> Integer -> Integer
foo p x
| x <= 2 || odd x = 0
| otherwise = head [i | i <- [x, x-1 .. 1], (p i) && p (x - i)]

bar :: Integer -> Bool
bar x = null [1 | i <- [x-1, x-2 .. 2], s <- [x, x-i .. 0], s == 0]

These two subroutines are very simple, clearly terminating, and you can easily prove almost any property of interest about each of them in isolation. But now I claim that their composition `foo bar` never crashes (on `head`); can you prove me right or wrong? Feel free to "simply" reuse any proof about any of them.

The idea that properties compose and that you can cheaply reuse knowledge about components to prove stuff about their composition is just mathematically false. There are a couple of results I mention in my blog posts that show that. We know that if you have a composition of components X_1 ∘ ... ∘ X_n then the cost of verifying some property of their composition is not only not polynomial in n, it's not even exponential in n (it's not any computable function in n, I think). I.e. it is a mathematical result that you cannot, generally, hide the complexity of components to make verification of their compsition scale with their number.
True freedom exists at the personal, inner level, each individual must earn it for themselves. How little Americans personally value the kind of external (political) freedom which they talk up as the absolute good and sacred can be observed in the 10% ish turn out rates in cities like NY and SF, as well as in how everyone tries to get out of jury duty as much as they can.
how about all that antibiotics they are being fed as well? this could be a man made problem.
Not if it is revenue-neutral.
New Tactics of Scamming People Online
>
If we're going to have censorship on the big platforms (Youtube, Facebook, Twitter, Reddit, etc.) and backbone providers (ISPs, Cloudfront), us normal human beings need the right to appeal, public auditing, bright line rules, and due process rights.

At least in Germany, people can sue Twitter and Facebook to have their accounts re-opened. Of course, this option reduces the value of due process rights as one has to be able to fund a lawyer and the court fees...
Nobody is well informed on all issues. You just can't be. You can't fact check everything.

We live in a world where the authority we defer judgement to has split up, into less balanced partisan entities. Not saying pre-internet news were unbiased, but public sources tended to be better curated. (At least where I live, I'm sure Fox has always been this horrid)

This is why filter bubbles and building psychological profiles for everyone to target them with political messages and free access to all information, correct and incorrect, does not work. It's a net negative to democracy and this neo-greek ideal of the marketplace of ideas is a sham.

I have no idea how to fix this, but it needs fixing.
Ups Has Been Delivering Cargo in Self-Driving Trucks for Months and No One Knew
Terrestrial Wireless Commun: Identifying, Managing Radio-Frequency Spectrum [pdf]
Evaluating Empathy in Artificial Agents
Same here, no offence taken. I found it funny how it seemed as if you weren't a programmer, but you mention naming things as something programmers can't do, which is something programmers say. It made me imagine an outsider who agrees with the programmers are crap at naming meme. "Those shitty programmers with their constant misnaming of things." like people hating on cab driver's anti-social driving.
While I agree that technically, fusion is not renewable, I feel like it might as well be? Working fusion reactors make it economical to siphon hydrogen fuel from Jupiter and such. Did you mean fission?
I did. I paid $240/year for Google One, which claimed to have support for consumer accounts. It was nice to have that peace of mind.

But then when I actually needed supoort, they couldn't do anything but read forum posts to me. They were not empowered to escalate to actually resolve anything more complicated than "where's the button for X".

Even if you pay, Google still treats their users like shit.
My point is, if your medical condition is causing the gas then reducing gas wouldn't help.
I'm more of the opinion that rewarding the reduction of emissions would work better than punishing the production of emissions.
> solutions that rely on substantially reconfiguring living patterns

Surely switching to bikes or electric bikes is not that substantial and immediately eliminates a lot of car related problems.
That hasn't been my experience so far, but I'd be interested to read in more concrete terms exactly what level of type-level invariant expression begins to create overly-rigid software.

FWIW, I'm not suggesting moving everything possible into types. I'm suggesting types are better than not having them, just like tests are better than not having them.
Yes you are totally right. JSX in itself and the way you can nest React components, etc is very nice and could be great as a template engine. I should have said more clearly that I meant React et al. in the context of rendering everything on the client-side.
HK youth getting Cambridge Analytica'd for the sake of the trade war by the usual actors.
Assessing the Global Climate in July 2019
Key insight. Very closely related. In the secularized instance of it we're encountering now, people could be said to be substituting demonstrations of belief for mercy, etc. I'd argue the particular choice of symbols in a religious war is really secondary and not meaningful to how predictable its progress is, sadly.
Bitcoin's Biggest Competition: A 105-Year-Old Nonprofit?
PulseAudio and systemd and avahi and probably other things he's been involved in solve problems I don't have, in intrusive ways, poorly and with much churn. It's not unreasonable to loathe someone who makes me wonder what exciting thing is going to break next in an exciting new way if i dare to update my system.
Rethinking Statistical Learning Theory: Learning Using Statistical Invariants
> "it becomes incumbent on the researcher to explain why no-one has noticed this before"

Farmer: huh, we'll I'll be damned. Who in the hell woulda thought to feed them seaweed."
The more comparable products are Sam’s “President’s Choice” and Costco’s Kirkland. Both of which have long developed brand promises that represent at least above average quality and some level of curation. Choice is a specific word chosen by Amazon to give the impression its products have similarly been curated. It’s deliberate subterfuge.
Bluetooth or an iPhone SE
We could put it down in empty mine shafts... or build entire mountain tops out of it!
To give some context. Historically React has been all about sharing what worked for us at FB for creating dynamic, complex apps. If it doesn't work well for you, please don't use it. There are plenty of alternatives.

The notion that there's some kind of plan to "weaken the web" there just isn't true. I don't know what you're basing it on. You may not remember this, but when React came out, everybody laughed at it. It was not some kind of asset for Facebook at the time. If we talk about motivation, ours is quite the opposite. We want to empower web developers to create complex UIs, comparable to native apps. We very much want the web to win, or at least to stay relevant.

The only reason React got open sourced and kept being developed in the open was because engineers working on it wanted to share it with the wider web community. They saw something useful in it. Eventually, the industry took note, but it wasn't until a few years later. We believe in open web, and this is why we work on React.

The notion that React is at odds with accessibility is also mistaken. React outputs regular DOM, and common React setups like Create React App include more accessibility checks than you'd get writing HTML by hand. Maybe you're confusing React with something else?

Yes, keeping dynamic JS apps accessible has its own set of challenges (we document some here: https://reactjs.org/docs/accessibility.html), but it's not React that makes it hard. It's the dynamic UI expected by users that makes it hard. If anything, in my experience React makes it easier for teams to adopt better accessibility practices by putting them directly into React components (example: https://ui.reach.tech).

Finally, concerning standards. We've worked and will continue working with standards committees to bring good parts of React into the platform. For example, the "object spread" operator in JavaScript was originally added to JSX, and was championed in TC39 by a React team member. Similarly, we're closely working with standard bodies to improve web app responsiveness. Not just for React, but for all libraries. You can learn more about this work here:

* https://github.com/WICG/is-input-pending

* https://www.youtube.com/watch?v=mDdgfyRB5kg

Happy to address any specific concerns if you have them.
The Hong Kong protesters’ anarchic campaign against China
Formally targeting people with medical issues makes your device a "medical device" and adds extensive certification delays. If you make something that's "totally just for weekend warriors" but it's useful for people with medical issues, they.. can still use it, but since it's not being marketed as a "medical device" the onerous FDA approval process isn't invoked.
I sit always in half-lotus.
speed limits serve a very important purpose. set them so that most people will speed and now you can pull any of them over at any time.
"but I wouldn't expect any free service that involves a paid employee from any service I don't pay for (with money, not privacy)."

It's not a free service. It's a surveillance company that spies on, profiles, and sells out its users for a profit in exchange for the services it offers. Most surveillance companies with email offerings have support. If Google doesn't, then it's taking something in exchange for nothing on top of doing less than the standard most of its competitors set in this area. It will also probably keep making revenue on the locked account for a little while despite its owner having no access.

Way different ethically or professionally than a situation where the user was getting free email with the other party getting absolutely nothing in return. Something truly free.
- https://medium.com/@schamne/why-your-choice-of-programming-l...

- https://www.codementor.io/agustinchiappeberrini/why-the-it-d...

- https://www.quora.com/If-truly-programming-languages-dont-ma...

- https://spin.atomicobject.com/2015/07/15/language-doesnt-mat...

- https://learnpythonthehardway.org/book/advice.html

The idea that programming language does not matter is a pretty commonly-held view.
https://www.washingtonpost.com/news/tripping/wp/2018/03/27/c...

>Researchers at Johns Hopkins University and other institutions who studied Stockholm’s congestion-pricing scheme found that the policy cut air pollution in the city center and reduced childhood asthma cases by nearly 50 percent.
I'm troubled to disagree with your comment, because I usually get so little feedback to such opinions and also it makes it look like I'm CCP stooge. So I should add that I'm British, I just lived in China for a year.

Your comment really worries me though, because it seems to me you're conflating the subculture of Guangdong with the culture of Honk Kong, perhaps in an attempt to make a tenuous argument that it is in fact Guangdong, like Taiwan, of which HK is but a tiny part, that desires independence. I think that's dangerously disingenuous to suggest that HK's current political consensus is but a facet of the wider Guangdong region's political sensibilities. I don't see any evidence whatsoever to suggest that what has happened in HK would not have also happened to any other port on the cost of China. HK wants independence because it took on the subculture of Britain not Guangdong.
Hey jrv, here's 2 resources for you to get more inspiration:
http://bit.ly/airminersresources
http://airminers.org

this is you: https://m.youtube.com/watch?v=ABg0c_E7OOI

looking forward to your application once you finish your training.
In Q1 of this year, twitter had 68 million monthly active users in the US [0]. Hard to tell how many of them follow political discourse. But that’s 20% of the population (give or take) and it’s a substantial fraction.

I’m not sure how but I want that fraction to get before appropriate rights are defined and adopted.

The US common carrier rules were only enacted in 1934 [1] so it took a while before phone companies were forced to respect some US rights. Twitter is only 15 years old so it’s likely that this private company (and others) will be regulated just like the private telephone companies were regulated.

I had hoped that technology had advanced enough so respecting human rights would be embedded into the design. But now I think it will take laws and regulations which will inevitably, and sadly I think, also squelch innovation.

[0] https://www.statista.com/statistics/274564/monthly-active-tw...

[1] https://www.law.cornell.edu/uscode/text/47/201
The president of the United States.
> SystemD

For those not attuned, writing systemd as "SystemD" is a dogwhistle which comes from a time when Lennart specified that it wasn't meant to be capitalized, and this crowd went the other way just to spite him.

Top bantz here, kids.
Great, but that's got nothing to do with a specific company, and it's not for Apple to do.

It's for us to vote for representatives who will implement better taxation and finance and safety net etc. policies, that result in better wages etc.

Criticizing Apple is a distraction. Criticize your representatives and vote.
Dimsum Daily is not exactly a good source for reliable news...

There is indeed quite a lot of violence from both sides, but no, no police officer has been set on fire.
I understand the issue, but you either committed insurance fraud or you didn't.

Here's the evidence, counter it and let the jury decide.
I feel your tone is drawing downvotes which is really frustrating because I think the discussion it is drawing is worthwhile (imho)

Can you work on adopting a less flame war-y tone?
Quality products likely have better margins.
And a product that will help give Malaysians lung disease
> Methane is a gas with a distinct and noticeable smell

Methane is odorless
https://en.wikipedia.org/wiki/Methane
Mathematicians a Hot Focus of Nationwide Job Postings
I'm not weighing in on whether these kinds of tweets should or shouldn't be allowed, but genuine question: how does this violate rule #1? Is it the use of the word 'cunt'? I don't see how the harassment was based on race, ethnicity, national origin, sexual orietntation, gender identity, relgiious affiliation, age, disability or serious disease.

Potentially that Palin is a woman, they've decided that 'cunt' could be based on gender, however I received the same email from Twitter for a (heat of the moment) tweet about Ajit Pai where I called him a cunt, and he is not a woman, so I don't understand their policy. They wouldn't unblock my account until I deleted the tweet.
heck yeah let's do that! Solar tech has gotten so much cheaper and better, my friend is replacing what used to be $30k of panels for $2k.
Not necessarily to extinction but to loss of control - I mean, becoming peaceful often means not investing in defence capability thus becoming weak, and becoming weak means inviting violence by opportunistic neighbours or inside groups.

It's a coordination problem - as any subgroup of homo sapiens that unilaterally abstains from violent power risks simply being overtaken by another subgroup that doesn't; you can abstain from using violence, but you can't unilaterally abstain from participating in violence started by someone else. "Si vis pacem, para bellum" will be true while humans are built the way we are.
But muh followers need muh rageposts!

"Everyone gets a platform" is not a right. It's never been a right. If anything, I hope it's a societal anomaly that we fix in the next 10 years. Again, the first amendment gives you exactly fuckall protection on twitter, and that's how it should be.

The New York Times isn't required to host your "Obama was the REAL racist" diatribes and Fox News doesn't need to have you come on every weekend to point out "Trump is probably a rapist" because you're not entitled to this. Same as Twitter.

That said: ToS enforcement is always difficult, always subjective, and always "unfair". There is no good way to fix this. Whatever cool idea someone has for how to fix this doesn't actually fix this. And they don't need to. Twitter gonna ban what Twitter gonna ban.
You are completely missing the point with your example and it's in no way similar to what's happening here. Free to use and free to sell are completely different concepts.

Just because someone gave you the right to use for free something that belongs to them doesn't mean you are allowed to sell that right or that "something", or even pass it on for free.
> 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.

Cost isn’t the issue, it’s mainly the fact that Autodesk effectively put Maya on life support. Pixar is paying hundreds of software engineers in the Bay to develop their proprietary animation tools, which is most definitely not cheaper than a few hundred Maya seats per show.
Hedge Funds Have $500M Riding on PG&E Paying Bills
تسليك مجاري الكويت للايجار
It's not just a re-brand as in "AMD is now making whitelabel CPUs". AMD gave the IP away for the short-sighted amount of $300 million, so now the Chinese can build their own Zen-class CPUs and create new variations of it.

And people wonder "how the Chinese have caught up so quickly?!". The western companies mostly gave away their entire IP for peanuts or some empty promises of "gaining access to the huge Chinese market", which never materialized because China made sure the local companies would always win. This, in combination with China's own theft of IP, is how they did it.
A publishing tool that can mimic private communication tools. Not for well thought out letters but for words spoken in a conversation. Which makes it so powerful. Which makes it so problematic.
I could be splitting hairs, but to me, guilt is established by another party, and something you may or may not recognize, whereas shame is mostly sourced internally. Someone, including the government, my employer, and other people, can declare me guilty of something. I also can admit guilt, but its not required. Shame on the other hand is something that only exists if I personally feel it.

I do agree with the notion that this may be somewhere close to one of the major differences between Western and some Asian societies (I'm thinking of Japan primarily, as that is what I have experience with, so this may not extrapolate to other Asian cultures). In Japan, I was shocked at the low crime rates. I could leave my bike unlocked pretty much anywhere and not worry about it being stolen. They leave vending machines on random alleyways everywhere with no fear that someone will break into them. Crime in general is just so much lower, despite opportunity potentially being much higher. Additionally, streets are so much cleaner than American cities. People don't defecate on the sidewalk. They clean up after their animals. Public transportation is clean and reliable and you aren't going to be screamed at by a homeless person. I think a lot of this comes from the fact that Japanese culture has a strong element of shame attached to people who transgress societal rules. In Western countries, the emphasis is more on guilt, which leads more to a culture of "getting away with what I can", and "its only a problem when I get caught". We litter more. We steal more. We are more violent. We tend to put less effort into our jobs.

Of course there are flip sides. I think the strong sense of shame and societal responsibility in cultures like Japan's also leads to more mental health issues, higher suicide rates and societal isolation. Tougher work environments and cultures. Sometimes a stronger apprehension towards challenging the status quo. I'm not sure if one is more ideal than the other. I'm personally a big fan of the societal cohesion that seems to exist in Japanese culture, but I have friends who found it stifling and sterile.
The fact that actual grown ups want to spend money on plastic caricatures of their favourite movie characters is fine in itself, but only if we also take responsibility of the state of the society we live in.

Replace "spend money on plastic caricatures" with almost anything and your comment still applies. "playing around with their computers", "reading books", "wasting time on social media sites like Hacker News" and so on.
Its not about security and privacy, its about obscurity and PR.

Corellium is heavily used by security researchers, killing it will reduce the number of bugs that are found in iOS and make the platform less secure overall.

Apple wants to project the appearance they have minimal security flaws and they accomplish this largely by making security research more difficult to perform.

I'm also confused why you seem to think security researchers don't deserve to get paid for their work. Bug bounties have been around for a while now for a reason.
Or garbage pail kids, or cabbage patch dolls. This phenomenon has been going on forever.
It's always been acceptable so long as it's directed at the right person. What's changed in the last 9 years is simply who can be targeted with such language. Twitter supports and publishes language like this on a mass scale today.
There's an interview to Neumann by BI where he talks about that exact same thing. Makes one wonder if they're betting it all on a recession for things to "work" (heh)

The interview, soft paywall: https://www.businessinsider.com/wework-ceo-adam-neumann-busi...

I don't like this pattern, more than VC funded startups they are more like QE funded startups, regurgitating your own devalued money as a favour. Uber comes to mind, too.
I'm sure he tried many times and failed too, and this is a later success. He does say he struggled to save even $5k, and this MRR looks like it took him 4 years to reach.

I think this is about risk; being a freelancer is relatively low risk (higher risk than traditional employment though?) and thus doesn't have higher payoffs.

There's also innovative ways that many "normal" freelance developers are able to earn $200k+/year. Maybe check their methods out and try to emulate what they did in your market? I'm sure you could find a clear path to reach their level with some self-training and practice.

I know it's difficult and scary, but that's just life.