skysight-inc/HackerNews huggingface dataset:
Yes, all sorts of industries have hidden subsidies. Airlines feed at the public trough too.

The airline industry doesn't have a habit of trying to convince you that flying is 100% safe though.
"Imagine a world in which logic, programming, and mathematics are unified, in which every proof corresponds to a program, every program to a mapping, every mapping to a proof!"

The thing I never understood about statements of this sort is that in my understanding of model theory, Godel's theorem and so-forth, a proof is a rare thing. Most of the true statements in a given model don't have proofs. Any consistent proof system admits an uncountable sets of independent theorems and so-forth.
Boeing Patents Laser Nuclear Fusion Jet Engine
> Avoid lazy transition calculations, and if you must use them, be sure to use specific properties (e.g., "transition: opacity 250ms ease-in" as opposed to "transition: all 250ms ease-in")

Why is it better to be specific?
Yii 2.0.5 is released (security fix)
> Confirm emails

Why?
Why would you say that? I've seen a lot of literature about damage done by psychopaths/sociopaths, but I haven't seen any on damage done by mislabeling people as such.

Without evidence to the contrary, I'm much more inclined to believe that more people suffer at the hands of psychopaths and sociopaths, than that people suffer from being mislabeled.
Sounds like the DoD asking for bids for a support for a product, which can only be legally fulfilled by the authors of the product

Why can it only be fulfilled by the authors?
reconciliation in my mind between dependent types and higher kinded types.

They are orthogonal concepts. This is made very clear in Barendregt's λ-cube [1]. Orthogonal here means that a typing system might be higher-kinded without allowing type-dependency, or it might allow type-dependency without having higher-kinds. An example of the latter is LF, the Logical Framework of Harper et al. Haskell, or at least some forms of Haskell are an example of the former.

Higher-kinded types simply allow functions and function application at the type level which can take functions as arguments and can return functions. For example (lambda x.x => bool) and (lambda xy. x => y) are functions at the type level.

An example of a dependent type is List(2+4)[bool], of lists of length 6 carrying booleans. Here (2+4) is a program. This parameterisation happens without having type-functions.

[1] https://en.wikipedia.org/wiki/Lambda_cube
Thank you Microsoft and Goodbye
The problem is that the law can easily place blame for big huge accidents but can't doesn't put any blame on massively distributed harm. A lot of the dangers of traditional fossil fuel generation doesn't stick to energy companies. They increase the chance you get cancer or respiratory diseases, but there is never a direct link. You'll never know if global warming caused a forest wire that wipes out several towns.

But when a nuke plant goes belly up, you know it ruins the small town it is in.

But the liability cap is part of a government enforced insurance scheme. It's a super highly regulated industry. It's not like they can ruin your house and stiff you.

The law is set up so nuke plants don't abuse corporate liability shields and then go bankrupt in an accident without paying for it.

Some claim it is a form of subsidy, but the government is allowed to retroactively raise rates if it turns out the risk profile wasn't accurately measured. It's really not that different from unemployment insurance companies have to pay for.

The reason it isn't just covered by private insurance is because when plants were first built, it was just impossible to underwrite. It still maybe hard to underwrite.

Insurance works on the law of large numbers. But with a low probability, catastrophically highly loss, it's impossible to insure.

If you exclude Chernobyl (and you should since modern nuke plants can't have a core explosion) there aren't any confirmed or even estimated deaths in the commercial nuclear power field. Even a super conservative estimate (no threshold radiation) would yield under 200 people world wide.

Shit, iPhones kill people than that a year (texting while driving)
i think correlation not causation
Right now its global already. https://twitter.com/telegram/status/619515927353278464
If only high schools took some time out of the 100% college prep curriculum to teach life skills like how to balance a budget and how credit debt and money worked... :)
Most true statements are uninteresting.
Geostationary satellites orbit much further away (~35,786 km) from Earth than non-stationary satellites (~2000 km).
Background tasks in Python 3.5
The obvious solution to the problem that I don't see on any of these message board sites is simply to allow users to have their own personal blacklists for blocking/filtering users whose comments they don't want to see. Personal differences aside the paid troll farms boosting the noise has really gotten unbearable on the interwebs.
Here, I'll address one of them:

"It is an extremely common occurrence for a programmer to accidentally forget to account for the possibility that a pointer may be null, potentially leading to (at best) crashes and (at worst) exploitable vulnerabilities."

Null pointers won't result in exploitable vulnerabilities in Go (not counting straightforward DoS-by-causing-the-program-to-panic). They might, in very rare cases, result in something exploitable in C or C++, because dereference of null is undefined behavior and the compiler is free to optimize accordingly. But in Golang the language semantics require the runtime to panic on nil dereference, so that won't result in something like RCE as it technically could in C or C++ (but isn't likely to).
I'll try to keep it short and skip the details of the mathematical framework itself.

Back in the early 1900's there was a school of mathematical logic that denied a certain axiom called the law of the excluded middle, that !!p <=> p. They said that if you used this axiom (roughly) your proof was not "constructive," whereas if you avoided it your proof was "constructive." They went as far as to deny all math that was not constructive (which I think is silly).

Their ideas faded out of popularity among mainstream mathematicians, but their goal was to rewrite the foundations of all mathematics using only constructive proofs, and to their credit they got pretty damn far in certain subjects like real analysis (calculus).

Today, their ideas are seeing a resurgence in the homotopy type theorists (HTTs). Their goal is also to rewrite all of mathematics in a constructive way, but now they have the hindsight of these great tools like category theory and homology and computers and all these great things developed in the mid to late 20th century. So they are working on building this framework and seeing what it can prove.

The HTTs are also claiming that proofs in their framework can be logically checked by a computer (because it is constructive) and one of their main selling points is that their work will eventually lead to "computer assisted mathematics," not in the sense of Stephen Wolfram but rather in the sense that a computer will check your proofs as you prove them and find stupid mistakes.

I personally am not all that excited about HTT, due to what I see as misguided hype around it. My preferred way to view it is as logicians studying a really fascinating new logical system and seeing how far they can push it. Saying things like "I deny all mathematics that's not constructive" and "computers will start doing our proofs for us," makes me cringe. But it is what it is :)
I'm sorry, but you're still missing the point. Yes, the nuclear industry could say to the government, "Please take away this policy that protects our industry." But the nuclear industry will not say that to the government, because the nuclear industry is made up of modern twenty-first century human beings who will happily rake in whatever government benefits are being offered and fight like demons to keep them from being taken away. You cannot make any conclusions about nuclear power's safety or lack thereof based on this.

May I suggest if you want to convince a group of grounded, knowledgeable, and technically minded people that nuclear power is unsafe, you're going to have to go with facts and figures, not "put your money where your mouth is."
Those interested further maybe interested to read :

Robert Scott Burn’s “The history of the steam engine” (1857)

https://books.google.co.uk/books/about/The_Steam_Engine.html...

Available in Google Play for no fee.

For a tldr: make a vacuum pump 10 feet across with unpowered tools
Have you or your wife had any big psychedelic experiences? If you haven't and your wife have that's probably the explanation. The Deep Dream animations trigger flashbacks like nothing I've seen before.
> This is how Java used to work, circa 2004.

This part of Java actually wasn't so bad. I would argue that Java didn't get better with the addition of generics in 1.5.
Why does that seem ominous? Genuine question. What would be a non-ominous response from the FBI in this situation?
StackOverflow is great, but it's audience is other developers, who may not be clients of yours. Does this forum have people who pay for services like yours?

I share my legal name with an engineer at Uber. Because of this, people who google me, will ask me about working at Uber.

People google your name, and covering the crap with frosting will help you deal with that event.
Encrypted Communication Is an “Ancient Liberty” Protected by the US Constitution
Apple’s Mac is now the only growing PC brand
This is the best answer so far. While some jurisdictions protect web admins from the actions of their users, others don't. So if you don't want to be extradited to some fascist state, you had better make sure that you can prove you have no ability to moderate or even know what content is being uploaded.
Please provide me your username, I'll check and make sure this never happened.
Sadly enough, that would be an obvious phishing ploy.
> It's really not as obvious as you're making it sound

It's as obvious as the fact that vaccinations don't cause autism.
>I'm not a Reddit user, but the vitriol seemed pretty commensurate with what motivated it, which among other things included the despicable (and possibly illegal) firing of an employee for having leukemia (more or less).

That employee got cancer in 2012. He got a salary for almost two years while too sick to work, of the total three years he was at the company. Four months of that salary undo Pao. Then he got an additional full year of health coverage when they finally couldn't wait any longer to fill his position. He was never well enough to even move to the Reddit officers, which was the plan when they hired him in 2012.

That's not just not despicable, it's laudable, and it's better than how you'd be treated at 99% of companies in the US. And somehow this became twisted by the furious mob into a story about a vicious CEO firing someone for having cancer?

(Legally in the US you are guaranteed three months of unpaid leave for getting sick. Although ironically in this case this employee didn't even qualify for that since he got sick before he was at the company for 12 months.)

That this became the battle-flag for everyone to pitchfork is appalling. Seriously appalling.
Stop treating citizens like consumers
You sound like someone that expects human beings in positions of authority to operate rationally.
Ahah, yeah, that's a quick bug we introduced today, you were able to join a table without paying the first blind :D
It's been fixed for a few hours now :)
Expired SSL certificate.
No -- it's just basic courtesy. Any criticism Mr. Altman has of Ms. Pao, he can share with her privately, and it's not privy to us.
Why We Encrypt
g2.steam instance type please.
Update: I just tried to get it to work and surprise! It doesn't work.

Somebody please just give me access to the PhotoDNA code, the hashes, and a little funding. I'll make an API anybody can use for this. It's ridiculous how hard it is to do this. It's still easier for people to get spam IP lists than to see if CP is being uploaded to their servers. You can't just have it available for Facebook and Google or it doesn't work, you need to make it available to everybody in an easy, simple way.

Seriously, if you are connected with this at all or want to fund this work please email me, I am more than happy to work on improving this: kyle@neocities.org.
Effective practices can work even if you have no idea why you're doing it that way. In fact, I'd say that that state of affairs is more the norm than the exception.
It's not elitist to think that the average HN reader doesn't need a reminder that you shouldn't blindly trust the media interjected into any random discussion that involves the media. Most of us read 1984 in high school, just like you probably did.

What's elitist is to think that the other camp only holds their opinion because they've been duped by the media, and that you're the one that's managed to see through it all with your superior scepticism, which is what generic_user is basically doing with their "The knife cuts both ways" comment.
I tend to think that in producing something like a programming language, it is really worthwhile spending a lot of time thinking and rethinking.

The language is a complex "artifact" with many surprises waiting within it. Wanting to go as quickly to implementation as possible seems like mistake - better to spend "debugging" one's syntax and semantics and underlying data structures.
Whatsapp could be banned in the UK within weeks
It looks like trolling.

If not - just try to judge people by work, not by popularity (popular people often are jerks). And be sure, they also judge you by work and also will not care abour your popularity.
Indeed but so are most programs.
But surely it is pretty simple to see the two separately - you pay X for electricity used (a falling amount) and Y for mandatory green tax (which everyone moans about but at least sees some social utility for)
Isn't this exactly how bacteria fights viruses? That is - by cutting known dna patterns using restriction enzymes. https://en.m.wikipedia.org/wiki/Restriction_enzyme
Chris Hadfield's ode to the ‘delightful impossibility’ of the Martian Chronicles
So why wasn't the NSA hosting this database? As cool as it must be to have XKeyscore and stuff, it would have been prudent to use some of those resources for securing this dataset.
You might be interested in the "circle" project some people are building on Ethereum, or perhaps a variant of it.

https://forum.ethereum.org/discussion/2228/circles-universal...

I think it might work better if trust was a number from 0 to 1 instead of a boolean, which would allow for different exchange rates, which would be useful if e.g. different sub economies formed separately with a different price for certain goods, so that the prices of the things with the different units aren't forced to change when the the two parts of the economy join into one.

I don't think I explained that well. To make a concrete example, suppose there are two collections of people/accounts, where each person/acc in a group trusts each other one in the same group (so that they can exchange their types of currencies automatically at a 1:1 rate). Suppose that in each of the two groups, there is a person who sells chicken drumsticks. If they are selling them at significantly different prices, then it seems there could be a problem if the two groups try to connect, because then one person could buy the currency in which the chicken costs less, buy the chicken, sell the chicken where it costs more, getting back more money, repeatedly, as an arbitrage thing. If it was just chicken this might not be a problem, as the two main chicken sellers would just settle on a common price for chicken, but if there were many types of goods, such that there was initially a source of arbitrage for every type of good produced in both communities, that seems like it would lead to problems.

A solution, I think, would be for when the two communities connect, by extending "trust", instead of establishing automatic 1:1 exchange, instead it could be made so that when a person trusts another person, they make it so that the other person can purchase up to a certain amount of their type of currency, at a cost of some amount that they choose of the trusted person's currency (an exchange rate).

In this case the exchange rates would be potentially asymetric, and there would be questions of "what is the cheapest exchange rate path to get personcurrency A from personcurrency B?"

and theres also possibilities of arbitrage in the trust trading of currency stuff, but the limit per time would probably reduce that I guess, and I think it would probably self correct (be EMH). IDK if that would be worse or better than with many types of goods and the exchange rate between currencies being forced to be 1:1, but I think it would probably be not as bad? I am not sure.

I'm fairly ignorant in this, but I thought the circles idea was interesting, and thought that a modification might be useful as described above. maybe.
No, you understand correctly. Living here, you pay, or the almighty tax authority will somehow get you in the end. This goes for nearly everything.
Official danish broadcasting channel, DR, collects roughly USD 350 per year from ANYONE with an internet connection worth the name.
Highly visible on Danish roads: We drive older, smaller cars than our Scandinavian and German neighbours. Decent cars are taxed out of reach. All in the name of sustainability and latter day puritanism, of course.
New Image of Pluto
> By extension of holding Pao responsible for all actions taken under her charge, I declare PG to be sociopathic, if not outright evil.

You don't think the downvotes are for this hyperbolic insult?
What are you attempting to say, that the images shouldn't be filtered because they aren't from the original source?
They recently updated their drivers and now support OpenCL 1.2 on recent GPUs.
previous discussion: https://news.ycombinator.com/item?id=9868331
CVE-2015-5122 – Second Adobe Flash Zero-Day in HackingTeam Leak
Well,

a) From my first reponse, I've been addressing your points. I haven't addressed every single last one of your points, just like you haven't done so with mine, because discussion works that way. Not to mention we'd end up with immense walls of text if we did. I just opted out in that last one, for obvious, declared reasons.

and

b) When the argument switches from arguing about a topic to arguing about the nature of the argument itself, it's boring. You can play semantic games into perpetuity like that. I've been arguing online since before the turn of the century; when it gets to this stage, it never goes anywhere, it's never interesting, and there's never any further insight to be gained by anyone.

My apologies though, I did forget your acknowledgment of the godwin stuff.
Typing systems (at least some of them) are also logics. This is called the Curry-Howard correspondence (CHC).

At first the CHC was made to work for propositional logic only, i.e. logic without for-all and existential quantification. Later typing systems were developed which correspond to logic with quantification. This requires dependent types. However, early typing systems with dependent types had an inelegant handling of equality. Logic needs equality to express things like forall x. x = 3 => x > 2. To overcome this problem, Per Martin-Loef introduced a dependent type-theory (MLTT) with "identity-types" which enables an elegant handling of equality. MLTT and all other extant formalisations of mathematics still suffered from another problem, in that many mathematical constructs are 'morally' the same, but formally distinct. For example you can define a group to be a triple ( G, 1, * ) where G is a set, 1 the neutral element and * the binary operation, or you can define it as ( G, *, 1 ). The former and the latter are not the same thing, but we don't really want to say that they formalise different concepts. This is similar to how in many programming languages certain types are formally distinct but somehow capture the same content.

Homotopy type theory (HoTT) overcomes this problem (or parts of this problem) by adding a single axiom to MLTT, called the "univalence axiom" which can informally be rendered as:

Things that are 'morally' the same, really are identical.

The key idea behind the univalence axiom is that MLTT (and hence HoTT) restricts the mathematical objects that can be constructed such that whenever you have objects O1 and O2 that are morally the same, then there is a function that transforms any construction involving O1 automatically into a construction involving O2 or vice versa, but in a truth preserving way.

It turns out that proofs in HoTT are formally similar to certain aspects of geometry/topology.

Much of current research on HoTT is about the consequences of the univalence axiom and the similarity between logic and geometry/topology.

The key hope in all this is that HoTT will streamline formalised mathematics.
> Somehow, we've gotten to the point that it is expected that everyone with a pulse is supposed to get a four year degree, regardless of ability to complete the studies necessary

The official taboo on the idea that a person might exist who lacks that ability isn't helping here.
That's why you search for "Golang" instead.
As someone how actually makes a living selling bioinformatics software, the problem is mainly due to how scientist view software. The code you write is seen the same way lab books are - basically raw data. Nobody publishes their lab books and all too often software is thought of as just an electronic lab book. It would be great if this changed, but it needs a change in how scientist look at software.
maybe, but I think that reducing the lifespan by 50% does not produce a reduction of 50% of the price for the seller, but often mean a reduction of 50% of the value of the product for the buyer. It is very bad also for ecology.
Always remember you could be wrong. This is the essence of humility.

And if you're thinking you're better than someone else, because of your résumé, or what projects you've worked on, or what school you went to, or where you grew up, or the color of your skin, or your gender, or your religion, or for any of the myriad other reasons we silly human beings come up with, then you're definitely wrong. On the other hand, no one else is better than you, either.

Learn to be alert to your ego. Don't let it get away with anything.

And if all that fails, learn Lisp! (Just kidding! Lisp users have a reputation for arrogance that is, alas, perhaps not entirely undeserved.)
Can I suggest not browsing all
Pretty much everything of the Java ecosystem is open source and I don't think there are organizations that wont use any open source code written by other people.
The GPU alone costs $2k. The CPU they use costs $1.5k, and is split in two between you and another user.
Agreed. Reddit is, unfortunately, a cesspool now for many reasons.