skysight-inc/HackerNews huggingface dataset:
That is basically the pitch for Metamath Zero[0].

I'm philosophically aligned with you. Basically, I think this is because of where resources are invested - there's a tremendous amount of work on programming languages to make them ergonomic and enable composition of pieces. Much of that work is at its essence processing friendly syntax into some form of typed lambda calculus. Since dependently typed lambda calculus is a very handy way to encode proofs, it's easier to just adapt that all that mechanism than to develop infrastructure just for proofs.

Interop is hard, because all the axiom systems tend to be subtly different in ways that are hard for normal people to appreciate, though there is some work on it, including MM0.

[0]: https://github.com/digama0/mm0
well if you think about it, there aren't very many people who are fully on-board with any given cryptocurrency, conceptually, who don't also have literally vested interests in said cryptocurrency. when you have literally vested interests in something, you're going to be defensive about your investment, possibly to the point of emotional irrationality. this makes conversation between the invested and the skeptics pretty useless most of the time—if a skeptic were to convince an investor that their cryptocurrency is bad, then they would pull out of investing in it. if an investor were to convince a skeptic that their cryptocurrency is good, then they would likely also become an investor.

put another way, there are broadly four possible types of people who would discuss cryptocurrencies on a website like this:

A) crypto fans who have invested in crypto

B) crypto fans who have not invested in crypto

C) crypto skeptics who have invested in crypto

D) crypto skeptics who have not invested in crypto

for obvious reasons, you aren't going to find many—if any—people in categories B and C, so that leaves categories A and D arguing with each other, and largely unlikely to change each others' minds—especially category A, because, again, they are literally invested in the thing they're a fan of.
> if 0.26% of tether is withdrawn into currency the coin would collapse

If 0.26% of Tether is withdrawn, it would need to start liquidating assets. That will, most of the time, be fine. Commercial paper is exceedingly liquid.

But sometimes, the liquidation will prompt a price fall. This is a fire sale. That, in turn, prompts more redemption, as holders of Tether grow concerned about its stability. This is a bank run. If Tether has a safety buffer between the value of its assets (U.S. dollar money market securities) and its liabilities (Tethers), this will--most of the time--be fine. If the situation spirals, however, a bank run can lead to collapse.
Seems to be part of SONET and CDMA 2000 standards to keep network elements synchronized:

* https://www.gps.gov/cgsic/meetings/2012/weiss1.pdf

Specifically frequency and phase sync requirements:

* https://en.wikipedia.org/wiki/Synchronization_in_telecommuni...
Study it a bit while it's still warm and look up your local weather. [1]

The COP gets worse as Delta(T) increases and heat pumps are nowhere near the theoretical best, so at a certain point it's better to use gas. But that's typically below 0F (-10C).

I put in a four way Mitsubishi (2x as expensive but super silent) in my old home. Relatively happy with it, except I don't think the installers put enough coolant in it (it's best to instal a heat pump on a cool day). The air does gets a bit dry, so consider getting a heating humidifier for the night.

Finally, if you can afford it and if you can install it, a heat-pump with buried coolant lines really multiplies the efficiency (since the ground is above freezing and acts as a heat store through the seasons)

EDIT:

[1] If you live near a large body of water, especially if it's salty, it's very unlikely your cold days are cold enough to be a problem for the AC. Unless you live in Thunder Bay.

[2] AC is not a huge climate problem. Heating, cars, global supply chains, agriculture are bigger problems. AC just gets the attention because it's considered frivolous. A bigger problem is that modern homes are built with no consideration for cooling. My old house was 100 years old and naturally kept cool. My new house has at least 7 seven!!! skylights. It's impossible to cool. At least 5 of them face north :S
My current company hasn't really had a harder time finding Elixir devs than my last company had finding Rails devs.
It would be a good start if any clear hate speech and very personal attacks would be moderated and prosecuted regularly.
Correct. They just offer their services exclusively to people that want to win elections.
The problem is that wet-bulb temperature is not the Heat Index or a "feels-like" temperature. Here's a bit more info: https://www.weather.gov/source/zhu/ZHU_Training_Page/definit...
You would think there would be traditional solutions for that, why not a put a cart full of dark stones in the sun during the day and then roll it inside in the cold of night? Modern variations on that theme could store thermal energy in plenty of equally-simple ways.
> I always feel like I'm in a different plane from the rest of the universe when discussing these things.

Exactly! It really feels like there's this massive disconnect in these conversations that I can't explain.

Whenever I have to use macOS, I'm a complete mess, and to me like it's missing basic features and doesn't support my workflow without lots of 3rd party add-ons, etc. That said, I probably am using it wrong, so I don't go around saying that macOS desktop is obviously garbage. I know that other people prefer this style, so that's A-OK.
You're right, "connected" can add more clarity.

For the automation of some govt systems, you didn't try a "proper" reverse engineering where don't use selenium, but rather uncover the private APIs of the govt ?
"Bugs are law" :))
Social media made the promise that it can handle all the big meanies.

The only people who are surprised and upset that social media was unable to stop or reform the human condition are those who genuinely believed digital technology would conquer everything.

No amount of bits will stop human discontent.
Prob not but itd shake everything up. They'd have to get a lot of loans, and maybe sell out the company. For comparison, banks allowed to go as high as 10:1 so 383:1 is insane.
You need Dashbird in your life if you're building on AWS
> YouTube indicated that examples of the offending content in the video included the line: “Most of the masks you get over the counter don’t work. They don’t prevent infection.”

> It also included the quote: “Trying to shape human behavior isn’t the same as following the actual science which tells us that cloth masks don’t work.”

Regardless of what you think about YouTube's misinformation policy, I don't think this is even misinformation! Seeing platforms control the narrative to this extent is truly fascinating. I never thought it would be as overt as it is. Tech companies feeling competent to dictate truth is scary.
It's almost unanimous that the general "null" from C is a very bad idea.
I mean yeah, but it's still a large complicated task. I don't think executing major projects like this should be handwaved because there's alternative options.

This is equivalent to saying there's nothing special about biontech as any specialist in novel MRNA vaccines could have developed these. Which did happen, at moderna.
This looks so tempting but each time I try to use something to avoid Javascript, I end up spending more time debugging the Javascript.

In your experience, how much time do you spend in the JS layer?
Banning select politicians on the digital public town square is the same as making a campaign donation to other politicians, except without appropriate controls on the funding.
One kind of building that I came across is called an "Earthship", which relies on "thermal mass construction and natural cross-ventilation to regulate indoor temperature".[1]

It will be somewhat difficult to retrofit buildings to take advantage of e.g. thermal mass inertia, but I'm hopeful that new construction will increasingly favor passive/low-energy cooling methods.

[1] https://en.wikipedia.org/wiki/Earthship
I mean the whole wheat bread I eat everyday is sliced, mass produced, and sweetened a little bit (as are almost all whole wheat breads, regardless of whether they’re mass produced) - I’m pretty sure it’s as good for me as any other whole grain.
Ventriloquism
So if Rand Paul is democratically elected and YouTube silences him, then in effect YouTube is silencing the population that elected Rand Paul.

Furthermore (I can't see the video) - if he did indeed simply quote two peer-reviewed papers is it right to suspend him?

As an exercise, which of the following statements are correct:

1. Gaiter masks will stop you from getting COVID-19

2. Surgical masks will stop you from getting COVID-19

3. KN95 masks will stop you from getting COVID-19

4. N95 masks will stop you from getting COVID-19?
The interest bearing accounts on the stablecoins are the (edit: things analogous to) MMFs, not the stablecoins themselves — at least for backed ones like GUSD and USDC.

Edit: not sure why a basic point is downvoted, I updated to clarify.
That sounds awful and certainly not what I was thinking about in the GP post.

That's not to say that having a persistent log of communication might not expose someone's pattern of lying. If it did I'd definitely incorporate that knowledge into how I interact with that person. It's not something I'd ever state explicitly, nor that I'd necessarily tell anybody else, but it would be factored-in to how I deal with that person.
The Git staging area, the term literally everyone agrees with
The human body can generate heat by eating food, it's just a matter of insulation to stay warm. Our bodies can't generate cool at a wet bulb of 35C. That's a huge difference.
Relevant: https://youtu.be/Y8RfeAmLfn8

There's also all the body heat, and the resistive braking of the trains which is being phased out.
Total means that the function must always return a value. In the presence of coinductive types and corecursive functions, a total function can run forever but must always be producing values when asked. e.g. an infinite stream of prime numbers can be produced by a corecursive, total function. You can use this to embed Turing complete computations in languages like Agda or Coq[1], they just must be declared as such up front. Much like IO must be declared up front in (idiomatic) Haskell. And much like you can unsafePerformIO in Haskell, Idris and Agda have their own escape hatches as the sibling comment mentions.

[1] https://strathprints.strath.ac.uk/60166/1/McBride_LNCS2015_T...
That's an excellent question, the ml modelers should ask those questioners themselves. There is a comment in this thread that in Spanish languages asking for a black ink cartridge (cartucho de tinta negro in Spanish) for a printer is automatically blocked because the word negro in hate comment is the word that has most signal for the classifier
Webview is not a replacement.

Webviews for GUIs is the worst of all worlds. You're packaging up two separate event based runtimes, chromium and node, and have no ability to interface with V8, meaning youre actually losing significant performance by having to serialize/deserislize data from node, to the browsers window, then deserislized on message in the browsers packaged JS engine.

It makes no sense to treat your desktop GUIs as closed sandboxes, what's the threat model?

Electron is not simply chromium, it has a bunch of optimizations, fixes, and prebundled functionality.
Maybe he works at Amazon
What's next, like, spank them? I really don't get why YouTube is not treated like all TV stations
There very much is an economy, and people vote based on how they perceive its health. There are certainly elites who have invested quite heavily in convincing people that policies they personally don't want enacted would be unhealthy for the economy, but that is an effect of public policy becoming wholly subsumed by economic concern, not a cause.

Saying the economy is a cover for the elites to manipulate the masses is like saying sex is just something advertisers made up to sell beer. They are taking advantage of a situation, they didn't create the situation.

The fact is that a carbon tax would be a new line item on the everyman's bill. It's fewer dollars in their pockets to go out and spend on all the things they want. Less consumer spending means lower employment, more foreclosures, higher debt, increased demand on public services, etc. All things people legitimately don't want. Even if it is for a good cause, our style of democracy makes such a proposal political suicide, even before elites start throwing their weight around.

And frankly, even the elites are mere pawns of the economy. The Koch family did not use their power to make oil profitable, the profitability of oil made the Koch family powerful. If someone finds a way to make solar panels print money better than oil wells then Big Solar is going to be able to outspend Big Oil on all these climate change PR campaigns. The smart elites on the side of Big Oil will switch over to the more profitable team while the dumb ones lose their elite status along with their wealth as they go down with a sinking ship. Being enthralled by people selected by the invisible hand is just being controlled by the invisible hand with an extra step.
Fast Estimation Method for the Stability of Ensemble Feature Selectors
‘masks’ is about as vague as ‘food’

There are good and bad masks, just as there is good and bad food.

A cloth mask will not protect you against an aerosol (note: am a researcher who has seen the electron microscopy images proving this), that is why N95s are mandated with no beards in any ISO work environment where you are subjected to aerosol risk.

The inability of public dialog on this nuance is just a reflection of our poor scientific education.
Indeed. Tech companies now silence politicians unilaterally, while governments made up of the same politicians do nothing to stop the widespread flow of toxic misinformation on tech platforms.

So, who is really in charge?
Hm wasn't regulation the problem that cryptocurrency was originally intended to solve? How does this regulation work for p2p transactions. The economist got one thing right, they are indeed a threat to existing systems of money, manipulation, and control.
Yes. With this, they're already doing that to his constituents in Kentucky.
Or you could use a decentralized and fully private crypto like Monero?
Kind has a "how I learned to stop worrying and love the `Type:Type`" vibe. That doesn't make it invalid as a proof language. It just inverts the priority: instead of consistency being the default and expressivity being opt-in (as in Agda, with the `type-in-type` pragma), it is expressive by default, and consistency is an opt-in. I strongly believe that is the right way. It is still not implemented, but the language is completely ready for that. About Type in Type specifically, keep in mind that there are consistent, interesting type theories that feature it. So it isn't problematic in itself, and removing it seems wrong.

About erasure, you can flag an argument as computationally irrelevant by writing `<x: A>` instead of `(x: A)`. So, for example, in the `Vector.concat.kind` [1] file, `A`, `n` and `m` are erased. As such, the length of the vector doesn't affect the runtime. As a good practice, you may also write `f<x>` instead of `f(x)` syntax for erased arguments, but that is optional.

> TL;DR -- I think the language looks nice, and the compile to JS (from what I read of the Formcore source) looks to be well done. Also, the docs that are present are well presented in a non-academic way that I find pretty readable.

Thanks for the kind words. We put a lot of effort on the compilers and, while there is still a lot to improve, I'm confident they're ahead of all the similar languages, by far.

[1] https://github.com/uwu-tech/Kind/blob/master/base/Vector/con...
I find it amusing that people are trying to downplay this because it is feasibly survivable in their opinions. If you're wondering "how I can survive these circumstances in my own home?" things are already really, really bad.
For buildings with central heat/air built in, I've often wished there was an additional function to either pull outside air into the system, or exhaust the air from the air return outside, ideally both. It seems like with all the ducting installed and a powerful furnace fan this would get you a lot of extra functionality with minor additional cost.
If I move to Luxemburg will they pay more?

This is the Nth article trying to convey the new narrative.

The narrative that "we need to go back".

No!

We don't need. The market is hot and we can choose.

Take the simple math. 1 hour commuting one way.

2 hours by day, 10 hours by week, 40 hours by month.

Working at home gives you back at least 40h.

Working at home GIVES you BACK AT least 1 Week!

And I am not even talking about better food, spresso machine and gym!

Now we are fighting climate change staying at home and reducing our carbon print not commuting.

Think of the children!
The masks aren't there to prevent infection, they are there to limit transmission. They work just fine for this objective, which is why the video was indeed spreading misinformation.
Banks are now required to have 0% of deposits as cash.[1]

It’s funny whenever people start to get outraged at seeing fractional reserve banking in any context besides where we’ve ignored it and accepted it.

[1] Citation for those who missed this development: https://www.eidebailly.com/insights/articles/2020/4/federal-...
You raise a good point about ageism... and perhaps the concept of tenure. My advice to young guns is that never rely on your employer to take care of you. HR is there for the Company...not for you. Most "lifers" I have worked with seem to have the same results as you, which does suck. But hey, you can be a martyr or you can avoid it by not sticking around so long. It does suck...and it is unfair, but it is reality. I suppose the exception are those "public experts" that have such an impact outside of their corporate sphere, that they can stay in the same job for ever. I hope you have great fun and find enormous satisfaction ahead!
I don't believe they want to ban encryption in the end. But I think it is prudent to make that accusation. This is politics after all.
The Sum is called Union in the TypeScript docs, as it narrows the valid values to the overlapping elements.

In the switch statement it becomes a Sum value (as shown in the article).

In ReScript (shown as well, which uses OCaml under the hood) the syntax is that of a Variant, in which each element is a different nominal type.
I found the video I actually wanted to post.

https://www.youtube.com/watch?v=sZ6cdLNWzlI

This is what happens when you don't have continuity/all the pieces.

Watch it and weep. Welcome to the misinformation age. John Perry-Barlow was right.

This was from 2011. They've presumably gotten a lot better at it now.
Apparently chat around the water cooler was the real source of all of their innovation. It’s worth $600 an hour.
I've seen people honestly believe than the world was black and white right to the middle of 20 century. You're way too optimistic.
Back when I was contracting it was common to see customers laying off their own staff towards the end of a project and try to keep the contractors. It was always a bit sad because the people being laid off usually knew the business inside out, the work couldn't have been done without them.

This sort of thing started in the eighties with Thatcher and Reagan. It's why I have never felt guilty about having a mercenary attitude towards work.
He did not. Watch it.
Personally I'd recommend to stay off of Twitter. The signal-to-noise ratio is depressing, even if you follow "the right people".

I've found more value in newsletters:
- https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-d...
- https://ethhub.substack.com/
- https://weekinethereum.substack.com/
As opposed to banks in the US, which legally have a 0% reserve requirement. [1]

[1] https://www.federalreserve.gov/monetarypolicy/reservereq.htm
Intel Debug Technology
The oculus quest 2 is only $300 USD and is the majority of headsets sold. I don't think tethered PCVR is the future but FB sure seems to be making a lot of progress here with mobile VR.
This seems exceptionally problematic.

I absolutely think everyone should use masks, but the science is clearly not in on the effectiveness of cloth masks. It's a valid area of discussion.

My own opinion is that everyone should use N95-equivalent masks, but others are entitled to their opinions too. We have democratic and civic processes to decide what should be mandated, what should be recommended, what should be discouraged, and what should be banned. Prerequisite to those is honest discussion.

What's more problematic is this doesn't even work. A good civic discussion convinces people. Simply shutting people up convinces no one.
The label of obnoxious behavior on TikTok is way too high for anything but light use. Heavy users of TikTok are definitely being negatively affected by it.
I understand the point of the downloading media over wifi rather than mobile data. What I'm saying is that once I'm "offline" I can't navigate to a screen where I can click play on them
>>They nearly took out the real economy in 2008.

No they didn't. The government nearly took out the real economy.

In the decade before the financial crisis, regulatory pressure was used to force banks to issue more subprime mortgages. This article from 2000 warns of the consequences:

https://www.city-journal.org/html/trillion-dollar-bank-shake...

Government sponsored enteprises, which underwrite 50% of the entire US mortgage market, started massively increasing their subprime loan guarantees at the same time.

And then you have Federal Reserve mouthpiece, New York Times columnist Paul Krugman, advocating in this 2002 article that the Federal Reserve create a housing bubble:

https://www.nytimes.com/2002/08/02/opinion/dubya-s-double-di...

"To fight this recession the Fed needs more than a snapback; it needs soaring household spending to offset moribund business investment. And to do that, as Paul McCulley of Pimco put it, Alan Greenspan needs to create a housing bubble to replace the Nasdaq bubble."

This revisionist account of the causes of the financial crisis is just these same powerful forces, who are receiving billions in kickbacks from all of this corruption, pinning the blame for the financial crisis on the mythical deregulation-bogeyman.
Isabelle is a generic proof engine, can be combined with any fronted which satisfies its API (it’s a bit more complicated) so yes such thing exists.

Proof assistants aren’t whimsical like cottage industry of programming languages. Proof assistants are divided into 3 parts, the core or foundation (F) which is a very small language at the heart of the prover, the vernacular (V) the language in which humans write the code and the meta language for proof search and meta programming (M).

The V is translated into F and this translation is often proven to be correct. De Bruin criteria says that F has to be small and should be independently checked (mostly through inspection or mechanization in other framework). In Coq the proof derives is again checked from ground up by F when you write Qed.

Andrej Bauer explains better than I can.

https://mathoverflow.net/questions/376839/what-makes-depende...
Note that Kind is NOT terminating by default. It takes the opposite stand. Expressivity is the default, so you can write recursions and loops freely, as in Haskell or any other conventional language. Consistency is a planned opt-in, which you may use to ask Kind's compiler to check for termination of mathematical proofs specifically.