skysight-inc/HackerNews huggingface dataset:
Interesting. For me, there is no clear gap between intuitive proofs and formal proofs. Sure, intuition can lead you astray, but as you do mathematics, you develop your intuition so that you stop being intuitively certain of false things. Contrariwise, formal proofs are more likely to contain dumb algebraic errors, but as you do mathematics you learn to be exceedingly careful in your calculations.

But the wider point I want to make is that there's no gap between the two. _Real proofs aren't fully expanded._ If you've worked with a theorem prover like CoQ, it becomes painfully clear how many steps even the simplest proof skips. For example, the proof that the sqrt of 2 is irrational is really easy:

https://www.math.utah.edu/~pa/math/q1.html

But look at how many steps this skips, if you want to get close to actual axioms and definitions:

- You squared both sides of an equation. In this case, that's fine because you're only doing forward reasoning, but if you wanted to reason backwards you'd also have to check that both sides had the same sign to start.

- You multiplied by q^2. That's only valid if q^2 is nonzero. Now intuitively we know that q^2 is nonzero, since q is nonzero. But it needs a proof.

- You deduced that p was even from the fact that p^2 was even. How do you prove that? My first thought is to use the fundamental theorem of arithmetic. I don't know about you, but my intuition completely glossed over the fact that the proof that sqrt(2) is irrational made use of the fundamental theorem of arithmetic when I first read it. Either that, or there's another way to prove this; what is it?

Now, you could expand this proof to include all the steps. But we don't bother, because it's painstaking and not actually that likely to catch flaws in the proof, because we intuitively know these things. Likewise, I feel like the triangle proof is the same way: it skips over some things, but we intuitively know it's okay and you could expand it (to talk about commutativity of translation and rotation) but there's usually not much reason to bother.

Although it's a lot more obvious how to go about expanding the proof that sqrt(2) is irrational, I'll give you that.
I have no idea, I'm just speculating wildly.
List by a Math professor: http://people.math.gatech.edu/%7Ecain/textbooks/onlinebooks....
Would love to know more about "Learning to control impulsive eating"
Doesn’t quantum mechanics leave open the possibility that our universe is fundamentally probabilistic?

Also, how can we say anything about free will when we have not come to grips with defining the hard problem? Of course, if you want to model biological processes based on deterministic physics then free will does not exist. I’m simply suggesting that the fundamental assumption that are universe is deterministic is flawed.
I buy my music, then I pirate a copy for archival and portable use. The artist and publishers get their money, and I get my fair use. I’m not willing to steal stuff, but I’m also not willing to jump through arbitrary hoops once I’ve paid. It isn’t strictly legal, but it is moral.
https://news.ycombinator.com/item?id=18099127
To enable them to be smoked cheap and easily - which in return means the user feels the effects almost immediately. Same reason why majority of users smoke rather than eat cannabis.
Through out it's history Russia has been far worse without a strong Sorpano at the top. Putin may me worth 50 or 150B and he came to power by blowing a few apartment blocks, but pensions, life expectancy, standard of living have sharply risen during his reign.

Maybe if the strongest cartel leader came to power in Mexico, he'd be able to eliminate most of the crime, but USA wouldn't allow that.
No. These are Bing results.
For syntax coloring in BitBucket, in Chrome at least, try the Refined Bitbucket [0] extension.

[0] https://chrome.google.com/webstore/detail/refined-bitbucket/...
I don't know, this sounds extremely specific to me. I mean, you'd think they'd know exactly whether or not their website works on Firefox, especially in these enlightened auto-update times.
Oh it corrupts... https://github.com/symisc/unqlite/issues/41
Yeah but that's because Rust is at the same low abstraction level as C++. So you have the same challenges in both, it's just that in Rust the gun refuses to fire when you point it at your foot.
Unqlite doesn't support in order traversal of data because the default (and only included storage engine) is based on hashing.
Not allowing people to talk about how you application performs is not compatible with GitLabs value of transparency. I've added a commitment to always allowing people to do this to our stewardship promises https://gitlab.com/gitlab-com/www-gitlab-com/commit/da81150e...
Let’s put this in perspective. Highly trained engineer, in 2018, decodes ancient diagrams, to fix a vintage IBM machine of historical economic, but little technical significance.

But.

The year is 1966. A 1401 at a Midwest insurance center’s card reader is acting up. It has been heavily used and is approaching obsolescence. IBM sends an a 20-year lifer, WW2 vet tech, making $7.50 an hour. He has seen this 3 times before. He opens that panel, switches the component, and it’s working. For good measure, he changes a number of other likely pitfall components, and cleans and lubricates the whole reader mechanism. All in 90 minutes, and he is gone.
What a heartwarming ending...

It's interesting to me just how alienated from male chimps that she never mated with any of them. My impression was that female chimps are much less selective or resistant to sex.
Url changed from https://www.ohcaption.com/news/201809-announce.html to the project home page, which is a better starting point for HN.
Torflow -tor network visualisation
https://github.com/jswanner/DontFuckWithPaste
Nope, not at my local theater.

I recently went to a small theater to watch a movie. It didn't start. After 10 minutes I went to talk to a manager. They had forgotten to download the licensed movie for the day and that download would take a couple hours. I had to get free passes to come back another time.
If nothing else, the cartels are highly incentivized to not harm tourists, as (copious) tourism money also flows into their pockets.
Even in weapons manufacturing there are “no go” weapons like around biological warfare where even the simple production is seen as bad.

I am starting to feel like this makes sense in other domains (namely, facial recognition has almost only applications with bad side effects in practice)
The reason that world has fewer full-fledged wars now
is major powers have mutual assured destruction, US-leading doesn't come close as that.
I generally try to get as much work done (in life) as I can. Some projects I can work for 12 hours a day on, others I'm tapped out at 6, so I just maximize output. If output is below the debugging cost of that code or something, I stop. Could be 2pm or 10pm.
I am with you on this. I find DDG completely unusable. The kinds of things that I search for are generally daily or weekly recent items and DDG never gets this stuff indexed quickly enough. Not even from the largest papers.

I am sure it’s fine for more evergreen content like SO, but for current news it’s awful.
Facebook hacked: Is it a good time to backup all your private data offline?
Facebook hacked: Is it a good time to backup all your private data offline?
I disagree with your disagreement - if China or Russia or EU or India where at the top they'll interfere in weak countries affairs as much as USA did/does.

If a country population and elites are unable to stand strong together, external forces (e.g. CIA) will find ways to promote foreign interests.
Facebook uses phone numbers you've never given them for targeted ads
According to https://www.nytimes.com/2018/09/28/business/elon-musk-tesla-... the original terms were

The plan, as it was negotiated by lawyers, was for Mr. Musk to step down as chairman of Tesla within 45 days and not resume that post for two years. The company, also a party to the proposed agreement, would add two new directors to its board. Mr. Musk and the company would pay tens of millions of dollars in fines, according to the people, who requested anonymity because they were not authorized to speak publicly.

In other words, it’s the exact same deal presented before with some of the penalties increased. There’s no other way to explain it than Musk rejected the real and then realized he messed up when the SEC started with the lawsuit.
> closing development branch when you merge into master???

Why's that a horrible default? It doesn't happen to match the workflow you use? It matches the one I use. So I can understand it's not ideal for you but they can't suit everyone with a binary default so what makes it so 'horrible'?
> Maybe the story is not true, maybe it is, it doesn't make it less insightful about the trends of the last decade about the emergent phenomena of massively profitable fake content publishing.

I'd say that depends. If this story paraphrases a bunch of facts we know to be true from other sources, then I see your point.

But if this story is not literally true, then we should be very cautious about using it as the grounding for other beliefs.
I think a lot of people are missing the point of this post, especially because it offers an opportunity to nit pick on specifics. But the point here isn't "don't write code for the military" or "don't write code for killing" or anything else, it's that we need to think about if we're okay with the code we're writing. We need to think about the implications of the things we build.

We're never going to find a hard line we all can agree on, aka "don't work on missiles, but airplanes are okay" or something similar. But we can all stop to think about what that line is for us personally, and if what we're working on crosses it. What would we do if asked to violate that boundary we've created for ourselves?

When I was in grad school, we had to take an ethics in engineering course. We split into groups and discussed the ethics of building certain things, in my group's case building predator drones. While I didn't agree with the person who said they were okay building them because we need weapons, I was far less concerned with that individual than the one who looked at me, straight faced, and said "I don't get what airplanes have to do with morals".
Can you share some resources to learn this?
There's another comment of mine on the thread, but basically, I doubt the small gang their interviewed has the big picture correctly (distressed gangs are not famous for correctly assessing the big picture).

Specifically, I do think they aren't correctly measuring their risks, so the gangs will fall, one by one, while all of them think they are making a great deal.
This is also a common struggle in South Asia and the Middle East as well.
That's !s in DuckDuckGo, FWIW.
Expensive damn tweet.
"Derailing him to jail time or prison would be a net loss for humanity, however objectively and legally inconsistent it may be."

The number one criterion for a functioning democracy is a reliable and consistent application of the law to everybody without exception. Declaring that somebody should be above the law is a very dangerous path.
So the same thing everyone already claims?
> so he’s very much in potential hot water

I don't think so. He was in much more risk before, with SEC investigation. The accuser in civil suit is asking for $75k worth of damages. I think Musk can pay off that fine and be free from it. I guess there will be no jail time. Although, i'm not a lawyer.
Theoretically BitTorrent should be more efficient, since peers nearby can send data directly (e.g. within an ISP or regional node), whereas a central server will always have to transfer a longer distance and involve more infrastructure.

E.g. with my ISP, the bottleneck isn't in the last mile (that's all GPON fiber) but rather in the national network and their transit to the internet. If more transfer was made to local-to-local, it would reduce the amount of traffic that needs to go cross-country or out on the internet.
For widespread distribution it’s a massive net reduction in traffic across internet backbones relative to centralized cervers. If files go from network A > B > C to two users on network C they can send packets to each other without going to networks A or B.

The protocol has quite a bit of overhead, so things can be worse among a small number of clients. It’s also worse than having caching servers on each network.
I think it’s a really interesting video, talking about race game programming (in the constrained environment of a game console), and how people manage to reverse-engineer it to discover some extremely large shortcuts.
Honestly? No. It's only ever been a small group of us techies and lefties that get outraged. The general public is far more likely to be demanding that Something Be Done. European countries with a recent history of fascist occupation or the Stasi have a much more intuitive understanding of the risks.
Plus, he’s still facing a raft of civil suits beyond the SEC, even beyond the one from the man he kept accusing of being a pedophile.

As I said, beyond that suit, i.e. the suits he’s facing over the tweets. And the DOJ investigation.
> For the love of God just use SQLite if you want an embedded database for structured data, even if it's just eav. If you just need key/value there are battle-tested, well maintained options.

You can also use the SQLite Disk Btree as a key-value data store. I've just implemented a solution that does so in C++ with a LevelDB-like api.

You should use the backend Btree api (the same the VDBE/SQL engine uses to store stuff) and create 'tables' the SQLite uses for indexes. The integer-key based is used for ordinary SQL table .. (1 PK = 1 Record) and the blob-key type, where its agnostic about whats on the key. (Thats the one you use to create the KV store)

There are a couple of details, to make it right, but its not that hard, and its a great solution.
I saw a small glitch where Apple Pay was offered as an auto-complete on the predictions bar in the 3rd slot but the actual auto-complete prediction was also in the same slot so the two things were on top of each other. Not sure if that was in the app or what but that's the only issue that I've personally seen so far since release.
Try “thrift books”, great source of old text books and cheaper than amazon.
There seems to be a link between Matrix fans and torrent technology fans.
Yes, thank you. Updated.
Yea, they didn't say anything about UX complaints, for which there are MANY.
Once I get 5 billable hours in the rest is just gravey. I’m a consultant though so I get paid by the hour.
Per multiple reports, the fine was doubled.
https://www.nytimes.com/2018/09/28/business/elon-musk-tesla-...

The plan, as it was negotiated by lawyers, was for Mr. Musk to step down as chairman of Tesla within 45 days and not resume that post for two years. The company, also a party to the proposed agreement, would add two new directors to its board. Mr. Musk and the company would pay tens of millions of dollars in fines, according to the people, who requested anonymity because they were not authorized to speak publicly.
>Be proactive - you see something you don't want the either use unsubscribe or filter them out (if it comes from the same sender, but most of the time they give you unsubscribe link which just works…).

I addressed this in another comment:

https://news.ycombinator.com/item?id=18102870

Consider the two methods:

1. Just have a whitelist that I've described

2. Be proactive in unsubscribing. If you buy something from someone online, be proactive at the time you buy in finding the box which says you will not receive pointless emails from them (not all vendors will have that option). Ditto if you or an app you want to run requires your email address.

My question to you: If I go the proactive route, what do I gain compared to the whitelist approach? Yes, I could be proactive and actively unsubscribe. That is time lost - even if it's not too much time for some people - what is gained by doing it?

>And to make e-mail a nice tool tune what you receive - if you get gazzilion of notifications that you don't read then just unsubscribe…

I think the difference between me and many of the commenters is this: I want my inbox (and my email usage in general) to be for personal correspondence. A few exceptions are OK, but I want the majority of the emails in my inbox to be personal emails. So it's not about a gazillion notifications. I probably get less than one personal email per day. If I get more than one non-personal email/notification/confirmation receipt etc, then my inbox is more noise than value.
>increase autonomy of all participants of the system

Yes, forced association causes bullying. There's no bureaucratic 'solution' that won't be gamed by the bullies. And there's no substitute for having good/brave people around the place.
QM is quite deterministic too, if you think of it like field theory.
i.e. the Inner Platform Effect (https://en.m.wikipedia.org/wiki/Inner-platform_effect), and all the worse for the programming being done without the benefit of programmers, in this case.
I do think so; 8, 16, 12 or 2 (with 12 being probably the easiest/most valuable). 10 is pretty worthless which is why it was adopted so late.
> critique

Elon Musk should not have said what he did, but advocating for sodomy is not critique. Some cultures have the death penalty for sodomy whereas the acceptance of critique is celebrated as wise in most cultures. The character flaw of the news is that in cases like this, it does not seek to create a peaceful resolution between the two parties, but instead blows up their differences as much as possible. Both of these men tried to save the lives of kids.

I agree that Twitter censure is likely to be of benefit to Tesla. Starving the news of Elon Musk content is a good thing. It will hurt the profits of attention-derived news. Plus, the doom of the ICE industry is rearing its head. So they can talk breathlessly about that and criticize the existing auto manufacturers for not seeing the writing on the wall once they figure out a new strategy to maximize their attention derived profits. I'm cynical enough that I figure this story shift will probably happen around the time that Tesla starts taking out television ads.
Cyrus Fariver has the whole document online, it’s an interesting read.

https://www.documentcloud.org/documents/4951792-828c547a-33c...
> I think I'm done with the tech industry. 98% of the sort of programming people actually pay you for is about as pleasant as a root canal. I'm currently on a sick leave and seriously entertaining the idea of changing careers to something entirely different. Like gardening.

More than a decade of professional software development later, I'm having very similar thoughts.

I now spend 1/4 of my work week fighting dependency hell (after just about each addition of a new package by any other developer on the project), another 1/4 figuring out how the "latest and greatest" tool of the week is best used to do something that would normally take me 5 minutes to do custom (god forbid, not the C-word!), and the remaining half is spent maybe doing actual work. So incredibly frustrating that I've just about had it.

I've grown to loathe and hate that which I used to adore.
You’re splitting hairs. Yes, you need to reason about escape analysis. This is pretty easy, especially since the compiler will tell you when things escape. It’s certainly easier than... well, pretty much anything in C++. :)
So this is currently fairly controversial in the cardiology world. This trial (COAPT) is tremendously positive, but only months earlier a very similar trial run from France, MITRA-FR, was dead negative (neutral).

Some of the authors of COAPT are trying to explain this by slightly worse valvular parameters and larger heart chambers. MITRA-FR also had a slightly higher complication rate.

However, my personal feeling is we need a third trial.
Thanks a lot for adding that!

This is a bit offtopic: (OP here) the reason why I was even reading Atlassian's terms is to understand what kind of language is used in enterprise self-hosted software because I need one for my own product. I really like GitLab's open core model (as long as the core is still perfectly usable), and I was wondering if I could ask you some questions about it as I'm looking to adopt something very similar? Could I contact you over email about this?
Actually these trials were about expanding Mitraclip's indications.

The old EVEREST trial resulted in it being licensed for degenerative valve disease (damaged valves), but here they wanted a license for treating otherwise healthy valves which are leaky due to being stretched open by a dilated ventricle in heart failure (functional valve disease).
Good point, that's going to help him and Tesla a lot. All his tweeting was distracting from the good things they are doing.
As a Rust beginner I am not quite sure why .min() is supposed to take ownership and change the sequence. I would assume it does nothing with the sequence except read it.
I just tweeted about this coincidentally. https://www.amazon.com/11-Filmmakers-Commemorative-Tony-Bena... is good watching multiple times.

Definitely anything Steve James has done too - currently America to Me (https://www.imdb.com/title/tt7768836/).
The mob in Japan runs Pachinko parlors.
Genuine question: he presumably has $20m of Tesla stock he can sell tomorrow if he wants. Since it's a public stock. Or $2m/day for the next two weeks. So what do you mean?

Sure he's not gonna sell all his stock... but in this particular case, it feels like a distinction without a difference.
>If an institution has lower number of incidents than population average than it's rather ridiculous to claim that it has an "institutional problem" with those incidents.

You can't draw any conclusions from the data presented in this article. It does not offer a per capita number of events.
Do they also require EME be enabled?
>We shouldn't just _accept_ the idea that other people / companies can assign us ongoing unpaid work for the rest of our lives.

This is exactly my perspective as well - I even said in another comment "I don't want to do this for the rest of my life". Reading the comments, it is clear not everyone has assigned the same roles to email as I have (which is understandable). For some people, opt in as a default seems to be acceptable.

I don't know - perhaps because I had email for some years without getting all these emails, I may simply have a different reference point than many who grew up at a time when communicating individually over email was the rare use case (as opposed to being notified of sales, meetings, etc).

(Note: Definitely not complaining or being sarcastic here - to each their own).
The proposal they previously rejected had an offer of no admission of guilt as well.[1] It's a very slightly worse settlement now, the apparent duration that he is barred from the chairmanship was increased by a year.

Most likely Musk wanted the optics of declaring himself innocent, rejecting the offer and feigning a fight. I'd be surprised if everyone around him have not been encouraging him to settle, the downside risk was far too great vs the modest settlement pain.

[1] https://www.cnbc.com/2018/09/28/teslas-musk-pulled-plug-on-s...
I think kerng's comment was motivated by the HN guidelines:

> Otherwise please use the original title, unless it is misleading or linkbait; don't editorialize.

In regards to your reply: Really? Everyone? The linked article provides little of value IMO. The claims are generally in line with what you'd expect from someone suing their former employer, and the publication doesn't seem to have done anything to investigate the claims.
For sure. Maybe you want to talk to Jamie, she knows most about this. Her email is jhurewitz at our domain.

Please have a https://about.gitlab.com/handbook/ea/#pick-your-brain-meetin... (public video) so others can benefit as well.

Please reference the url of this response in your email to her.
Nice, very tempted to give it a try. How do you find the ddg search experience on mobile?