skysight-inc/HackerNews huggingface dataset:
> Hence why they need results reviewed and a community to agree upon what's acceptable as a proof. Otherwise reviewing a proof would be an automatic process, if everything was done in the world of syntactic symbols with clear rules that tie one statement to the next.

Nonetheless, we may still get to the second case because there are a couple of large projects that are trying to formalize all of mathematics in a way that a computer can verify.

http://us.metamath.org/

https://arxiv.org/abs/1910.09336

If these catch on and become a deeper part of the mathematics research process, mathematicians would still discuss "what's acceptable" in terms of their views of axioms, and they would presumably still discover proofs for theorems, but review for formal correctness of inferences could be an automatic process.

Note that some pretty impressively complex and abstract theorems have successfully been formalized in these systems (and their proofs checked by machine), even starting from quite small axiom systems.

Edit: In the mathlib paper they mention a much wider set of efforts along these lines:

> In this section, we compare and contrast mathlib with other substantial formal libraries for mathematics, including libraries for Mizar [9,28], HOL Light [35], Isabelle/HOL [49], Coq/SSReflect [10,46], and Metamath [47]. Our goal here is not to provide detailed comparisons of the various de-sign choices, but, rather to sketch the design space in broad strokes, situate mathlib within it, and explain some of the decisions we have made. Our choice of comparisons is not meant to be exhaustive: there are also substantial mathematical libraries in HOL4 [55], ACL2 [42], PVS [50], and NuPRL [17], as well as notable libraries built on standard Coq, such as the Coquelicot analysis library [14].
You seem to be fixated on intentional seroconversion as an effective strategy we somehow "missed", but the experts (i.e. epidemiologists) seem to be pretty consistent that this is a poor strategy. Why are you convinced otherwise?
More nuance is needed; Rice's Theorem says that there is no formula for deciding any semantic property of an arbitrary computer program. Restricted classes of computer programs are totally fine, and in some sense that is exactly what a logical system is: a description of a restricted class of programs.

But this is also getting a bit confusing because there are many different interpretations of how to tie computability to a logical system. For example the proof system of first-order logic can be interpreted as a single Turing machine program, not a family of ones, for which it is very possible to make all sorts of judgments about its semantic consequences.
I don't want to be dismissive of the way you feel. I just want to point out that you have nothing to worry about. Now that AlphaGo exists humanity is exactly where it was before it existed. AlphaGo isn't intelligent like you and I are intelligent. It's just a program that's good at calculating the results of a very specific computational task. It's like crying because a hand mixer can beat eggs faster than any human can beat them by hand - there are many tasks that humans aren't the best at and there's nothing concerning about that.

Calculators have existed for a long time and they crush humans at doing arithmetic. I wouldn't cry if I watched a documentray where a calculator beats the best human at 5-digit-number multiplication. AlphaGo is like a big expensive calculator that's specialised to doing the calculation of how to play Go.
positive earnings == profits.

I am not questioning their profitability but simply pointing out that without the regulatory credits they would not be profitable. The linked earnings release confirms that the profits ($331M) are lower than the regulatory credits ($397M).
Most people disagreeing on most subjects have probably barely applied any sort of reasoning to get there.

Most pro-vaxxers have simply picked up the dominant opinion from the surrounding society -- not a bad heuristic in practice. Most anti-vaxxers have picked up an opinion from a persuasive single source and then read some other sources that back it up.

I admit I'm in the first category, I certainly vaccinate my own children, but I can't really claim that I've come to this decision after a thorough understanding of immunology, I have simply followed the path of least resistance.
I think Alan Kay himself has suggested that what he really wanted when thinking of OOP was something more akin to the Actor model as espoused by Hewitt and realised by Erlang and to a lesser extent Scala on the JVM.

This model gives full benefit of FP at the actor level whilst being realistic about distributed messaging semantics.

I’ve always felt that it would be interesting to research processor cores that could better exploit the assumptions in this model, and this would be the future of both multi-core and distributed computing. Actor message queues would be in hardware, there would be opportunities to reduce context switching overhead between actor activations, memory models would be more fine grained, capability based security would be ingrained.
DKIM was not designed to authenticate emails far into the future.

In fact, it does not authenticate any emails without a corresponding public key currently published to DNS. It provides specifically for "empty" or revoked keys to avoid such retro-validation.

Seems the central thesis is that because these messages are patently no longer authenticated by DKIM, we should eliminate any remaining hope of them being construed as authenticated by DKIM.
I assume that Apple's reasoning is "Userspace malware shouldn't be able to trivially intercept anti-malware checksum updates".

Trivially is defined as 'click an OK button in a dialog' as the CF permissions process works in Big Sur today.

Malware could still block anti-malware checksum updates with PF, but that requires sudo/root which is 'less easy' than the one-click CF approval process, and PF blocks break so many things on the system that malware can't get away with it without triggering a call to technical support.

(I personally think that much of the issue here is 'macOS background updates can cause $$$$ cellular data drain over wifi-tethered cellular', and that the absence of Low Bandwidth mode in Control Center is one thing that drives users towards these third-party content filters, when they might otherwise not need a third-party product at all.)
Where do you work that you can't watch a video? What's the reason?

Genuinely curious, not insulting/snarky.
Yes, You May Pee in the Shower
Show HN: Polls API – Fast and Scalable API to Build Polls, Quizzes and More
> i.e. not all people infected with COV-19 wind up with COVID

Nitpicking, but "not all people infected with SARS-CoV-2 wind up with COVID-19".

https://www.who.int/emergencies/diseases/novel-coronavirus-2...
....why have I never thought to put espresso in my cereal?
You're not far off on your numbers, they laid off around 1900 people back in May, out of ~7500 employees.

I would think the IPO is happening despite the pandemic, not because of it. They had been planning to go public long before the IPO hit, so I wouldn't read into that too much. I definitely have similar reservations about the company as you do though. I get the impression the tide is generally turning against the airbnb model at least within major cities.
> Sharp LR(3)5902

This really should be referred to as the Sharp SM83, as original Sharp documentation has now been found for the microcontroller that was used in the Gameboy's SoC.
My brother in law is from Marocco and always drinks coffee too.
I don't know, I liked the video but am uncertain of his hypothesis. If it was due to lactose intolerance wouldn't all the cheeses and pizza's enjoyed around dinner in Italy cause some major issues for many people? Also gelato? My guess is its due to caffeine and avoiding any ingestion of it for a long time before bed is a smart move.
More looking for an ETF
Mudge name handle does rings a bell and the main reason is that he was featured and interviewed in the arguably the most famous 49th issue of Phrack magazine containing the popular article "Smashing The Stack For Fun and Profit"[1]. In term of popularity this article is at least as popular in computer security circle in term of its profound effect as Dijkstra's seminal paper on "Go To Statement Is Considered Harmful" in computer science community.

[1]http://phrack.org/issues/49/4.html
WSL works, but it's not nearly as integrated as a native CLI in MacOSx. For example, accessing Windows files from WSL is tricky, the other direction as well. Don't get me wrong, it's definitely an improvement over what we had before, but the overhead is such that I still primarily seek out native Windows executables (was just installing JVM and Bison (parser generator) the other day).
Well they ain't doin' it.
"The point is – imagine a country full of bioweapon labs, where people toil day and night to invent new infectious agents. The existence of these labs, and their right to throw whatever they develop in the water supply is protected by law. And the country is also linked by the world’s most perfect mass transit system that every single person uses every day, so that any new pathogen can spread to the entire country instantaneously. You’d expect things to start going bad for that city pretty quickly.

"Well, we have about a zillion think tanks researching new and better forms of propaganda. And we have constitutionally protected freedom of speech. And we have the Internet. So we’re kind of screwed."

https://slatestarcodex.com/2014/07/30/meditations-on-moloch/
Nice dashboard!! Would love to see more details on the "Custom Data".
Uber is not that difficult. There's work for hundreds of developers between the few products, the localization for tens of countries with different language/currency/culture, and maintaining the main applications in working condition 24/7 at global scale. That's about it.

They have thousands of engineers sitting idle or making pet projects, struggling to justify their existence, as regularly attested by internal employees when an article pops up.
From the outside in, there are a lot of aspects of the legal system that look like this - welfare for lawyers. Unfortunately, fixing it requires changing the law and we've made of practice of sending a lot of lawyers to Capitol Hill who are very sympathetic to the needs of lawyers. It's probably the biggest self-perpetuating interest group there is.
It's much more tax efficient for Chesky to get loans against his equity in lieu of cash compensation -- especially if he believes that the equity will grow dramatically in value due to an IPO.
I believe this is what the page is referring to (The Dawning of the Age of Stochasticity)

https://www.dam.brown.edu/people/mumford/beyond/papers/2000b...
In case you didn't guess right away, yes, the title is editorialized. The content seems fine, though.
Yeah, whatever: I have one too; only 16 years out.

PhD is definitely a currency, and no they're not fungible: I'm trying to figure out which ones are actually worth something. In my experience it's a fairly lousy signal. Every Caltech PhD I've met has been sharp as a tack though.
Of course they do. But it still takes time, effort, and resources to run through the QA pipeline.
There is some more information at

https://jeffreykegler.github.io/personal/morgenstern.html

There's also an article about this question at

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=2010183
10k Hours with Reid Hoffman: What I Learned ( A Quick Summary)
How to deploy and scale a machine learning model on AWS Lambda
Macros for Domain-Specific Languages [pdf]
Show HN: Stop writing technical documentation. Use GenDocu
Developers hate writing documentation. We know that - that's why we are starting with beta version. You can join our secret club and be the part of the next big thing.
I'm comparing the M1 to a cpu that would have been used in a Macbook pro 13 if it weren't for the M1 soc. The current i7 intel Macbook pro 13 inch has the 1068NG7 model. Which is in fact a better cpu then the 1065g. Which is last gens 1165g. So I think this comparison is completely valid.
Body cams are an expensive diversion that tries to use technology to solve a legal, procedural problem. HN loves them, because hey, there are interesting technical questions about their deployment, but they accomplish nearly nothing.

The real issue is that even when police impropriety is discovered, with mountains of evidence to support it, oversight bodies have no ability to censure the officers involved.

In Seattle, for example, the civilian oversight office offers non-binding disciplinary suggestions to the only body that can discipline police officers - their union. Unsurprisingly, the union takes those non-binding suggestions, and puts them right into the paper shredder. On the county level, until quite recently, the oversight organization couldn't even subpoena records from the sheriff's department - it would ask the department to turn over records, and the department would kindly tell them to go pound sand.

The only other form of oversight is raising a criminal case against the officer involved. Because of the discretionary nature of prosecution in this country, and because of a huge conflict of interest, where 99% of the time, prosecutors work in tandem with the police, prosecutions are frequently sabotaged for political reasons. (See the Breonna Taylor indictment - where the prosecutor deliberately sabotaged the case he presented to the grand jury.)

And on top of that, the bar for a criminal conviction of a police officer is astronomically high.

No amount of body camera technology is going to fix either of those three problems.
Unsolicited advice: your problem isn't great - sure engineering leaders want to increase personal connections between remote teammates, but is that one of their top problems and how much are they willing to pay to solve it

I would iterate until you find a problem that people are willing to pay a lot of money to fix.
Wait what? Do tell, the links aren't great on my phone.
Mesoblast. I won't bother to share the full story of all this company's ups and downs over the last decade but let's just say that the amount of time I spent tracking the news on it was far out of whack with its importance to my portfolio.
Chinese spyware.
Also this JAMA video on the various types of coronavirus vaccines https://www.youtube.com/watch?v=KMc3vL_MIeo
Who's the other one? Microsoft?
IDK, put that shit in a properly insulated box stuffed with dry ice pellets, you'll maintain ultra-cold for three days easy with no electricity. So if you're loading a plane in Europe that spends 24 hours flying to $remote_destination, it still leaves you with 48 hours to do distribution by road, then you have another 5 days at normal freezer temperatures that is available for actually giving people the vaccine.
And never a flat white to be found. Sydney, Melbourne - great coffee culture when we lived there in ‘08, better than EU.
Good on the EFF. This is wonderful to see.
K3s is definitely more lightweight than K8s, but it still requires non-negligible resources. Compared to just a Docker engine, it takes more memory and CPU, which can be noticeable on smaller servers, Raspberry Pi, and such.
> Not everyone is law savvy. Not everyone understands legalese. Not everyone makes rational choices all the time.

> Does that mean everybody should suffer the consequences of an arguably unintentional side effect of the technical implementation of law?

Thankfully this is not law, but people should understand the things that can get them in serious trouble. A lot of legal concepts follow from basic principles and history.

Privacy concepts are the same way. It's simply not sufficient that we don't educate everyone about these things anymore. Ignorance isn't going to protect anyone from the fallout of misuse of technology.

The solution isn't to coddle people, it's to provide better technology that does the thing the way people intend to use it.
This is one of variants of an area called "score following" and it's really hard. I remember about 10-15 years ago there was this craze in start-up land which led to many corpses of start-ups who thought solving semantic music problems would be easy with FFTs. But forgot to talk to an actual MIR (music information retrieval) or Musicologist. I remember a friend of mine working for one about 15 years ago and when she describe their deal I was like "have you talked to a real music person? Because that is only going to get you a tiny part of the way there". Nope. And sure enough, dead in the water a couple of years later. I'm studying music cognition right now in a cross discipline masters (music, comp sci) and it is crazy complicated.

In a nutshell: the human brain has an amazing ability to separate a garbage pail mush of audio into meaningful streams that we perceive as different event streams. This enabled us to do things like notice (as my prof says) the difference in white noise between the nearby river and the rustle in the leaves from something else, like an approaching animal. Score following requires doing this to separate the aggregate noise into different instruments and into voices within that instrument, suitable for note by note analysis. This, it turns out, is a wicked hard problem.
I sincerely doubt a large portion of them are cut-out for the sector at all. That's the issue.
mostly because it' makes a lot of stuff easier. like database upgrades (no downtime), especially when google gives zero fucks in implementing pg_upgrade support.
also everything that @craigkerstiens said. (shamlessly point to his text)
I have tried k3s and microk8s. Recently setup ArgoCD, connected to our GitLab instance. Tried both Traefik and Nginx Ingress controllers. And so on.

And dokku is better if you want a PaaS.

There are probably dokku/heroku/deis-like things that run on kubernetes, but so far I haven't found 'it'.

Of course you can just run dokku on any k8s distribution. You can even use k8s as a backend for dokku instead of docker - https://github.com/dokku/dokku-scheduler-kubernetes
Apple probably
Loving this so far!

One tiny typo that threw me for a loop for a second was:

> when apples are a fruit, then bananas or applies implies bananas or fruits

which should be:

> when apples are a fruit, then bananas or apples implies bananas or fruits
There's a big difference between AWS Aurora and AWS RDS PG. Both are managed services.

Amazon supports PG 12 and 13 is in beta. Aurora is Amazon's fork of Postgres which has different storage and replication so will always be behind.
The following is a relevant quote from Clay Shirky.

http://www.shirky.com/weblog/2013/11/healthcare-gov-and-the-...

Back in the mid-1990s, I did a lot of web work for traditional media. That often meant figuring out what the client was already doing on the web, and how it was going, so I’d find the techies in the company, and ask them what they were doing, and how it was going. Then I’d tell management what I’d learned. This always struck me as a waste of my time and their money; I was like an overpaid bike messenger, moving information from one part of the firm to another. I didn’t understand the job I was doing until one meeting at a magazine company.

The thing that made this meeting unusual was that one of their programmers had been invited to attend, so management could outline their web strategy to him. After the executives thanked me for explaining what I’d learned from log files given me by their own employees just days before, the programmer leaned forward and said “You know, we have all that information downstairs, but nobody’s ever asked us for it.”

I remember thinking “Oh, finally!” I figured the executives would be relieved this information was in-house, delighted that their own people were on it, maybe even mad at me for charging an exorbitant markup on local knowledge. Then I saw the look on their faces as they considered the programmer’s offer. The look wasn’t delight, or even relief, but contempt. The situation suddenly came clear: I was getting paid to save management from the distasteful act of listening to their own employees.

In the early days of print, you had to understand the tech to run the organization. (Ben Franklin, the man who made America a media hothouse, called himself Printer.) But in the 19th century, the printing press became domesticated. Printers were no longer senior figures—they became blue-collar workers. And the executive suite no longer interacted with them much, except during contract negotiations.

This might have been nothing more than a previously hard job becoming easier, Hallelujah. But most print companies took it further. Talking to the people who understood the technology became demeaning, something to be avoided. Information was to move from management to workers, not vice-versa (a pattern that later came to other kinds of media businesses as well.) By the time the web came around and understanding the technology mattered again, many media executives hadn’t just lost the habit of talking with their own technically adept employees, they’d actively suppressed it.
And that's before even separating out by instrument! It's really quite incredible what goes on between the ear and the brain for this kind of thing.
You need to read up on Anemic Domain Model (https://martinfowler.com/bliki/AnemicDomainModel.html).

I see a lot of chaos in your post.

Model is a model. Model is there to represent an aspect or aspects of a real system (https://en.wikipedia.org/wiki/Conceptual_model). An object called "Employee" is a "model", a representation of certain aspect of an actual employee.

Object oriented programming is about using objects -- models (representations of aspects) of actual systems, actors, objects, etc. In OOP you build the model from operations that define the object. The fields are not part of the interface, the operations are. That's why everybody says to make fields public (but for some reason not everybody remembers why).

So a method call fire() on an object Employee is more "object oriented" than having HREmployeeService.fireEmployee(employeeId) to set field employedTo directly on EmployeeDAO.
Thank you for this link, this did not come across my radar.

From your link:

> The only way the email could have been faked is if someone hacked into Google's servers, found the private key, and used it to reverse engineer the email's DKIM signature, Graham, said.

https://www.zdnet.com/article/google-fixes-major-gmail-bug-s... is from Aug 2020 and discusses an SPF/DMARC vulnerability that was in Google since forever (and though reported 4 months before public disclosure, was fixed only 7 hours after public disclosure). The last google DKIM bug I'm aware of was in 2012, so I can't counter the specific claim about DKIM with evidence, but the assertion that "the only way to spoof x is to hack and get the private key" is not any absolute truth.

(P.S: I have seen no denial nor confirmation about the authenticity of the Hunter Biden data - only claims of Russian involvement. Make of that what you will. The DKIM is circumstantial data until there is confirmation or denial - especially, as you say, it's not all released).