voidmain

partial_sum has the same problems (eg when T - T isn't T) and would be more generic if it took the initial accumulator as a separate parameter (and then it and a more generic adjacent_difference would be symmetrical again)

I haven't thought about this deeply, but it seems to me that the evolution of unicode has left it unparseable (into extended grapheme clusters, which I guess are "characters") in a forwards compatible way. If so, it seems like we need a new encoding which actually delimits these (just as utf-8 delimits code points). Then the original sender determines what is a grapheme, and if they don't know, who does?

If you want to get an idea of what proving things in Lean is like you could try this super fun game, which I think is by one of the people behind the FLT formalization project:

https://adam.math.hhu.de/#/g/leanprover-community/nng4

I think you are right that the asymptotic claims are wrong, but it also seems plausible that hashing a k-byte string (in some way that gives you k prefix hashes) may sometimes be drastically cheaper than k cache misses in a large data structure. My charitable guess is that the author is implicitly using a cost model where only access to unbounded memory has a cost.

I think a type system that permits a type (no_locale=()) | (thread_locale=()) | (global_locale=()) | (env_locale=()) would generally be considered structural. I think newtypes and structure field names are isomorphic in functionality. Where a nominal type system would use newtype(tag,X) a structural one could use struct{tag:X} (and this holds even if X is the unit/singleton type).

The science is interesting, but it seems like the solution "go outside" is available regardless of the details?

I guess I wish the people trying to do this luck, but I'm skeptical they will succeed at getting broad adoption and remain any better in terms of privacy etc than "big tech". If your solution is "service first" you almost certainly have all your users' data and are in a position to rug pull privacy at any time, and business or politics may not give you a choice about it.

Sometimes I wonder if I actually want to use broadly adopted technologies. When my wife and I were dating, she volunteered at a kids' camp on a native american reservation. As she was being driven out to the camp by one of the permanent staff, she pointed out a cute bunny rabbit, and was horrified when the guy thanked her, took out a gun, and killed it. He explained that while rabbits are cute, where there are rabbits there are rattlesnakes, and you don't want those around kids.

Any medium capable of communications and adopted by most of humanity is going to be a war zone. Politics, propaganda, advertising, surveillance, addiction, fraud, child porn... all the rattlesnakes are going to go where the rabbits are. Someone ought to fight this endless tide. But I can't help but be tempted to look for a place that won't have an "eternal september" because it isn't easy to adopt.

There are 8 billion people in the world. If only 1% of them are even capable of signing up for something (because it's that hard) and only 1% of those bother, that is almost a million people, which seems like far more than I ever need to talk to. And I bet the quality of discourse would be better.

Maybe this world already exists and I haven't been invited.

The article says the spheres will be at 500-600m depth, so something like 50-60 atmospheres of pressure. Compressing air enough to displace water at that pressure would heat it to extreme temperatures which must be very inefficient even with some attempt to recover the heat. Water being incompressible can I assume be moved in and out of the sphere without any heating (and, therefore, energy loss).

(I'm guessing, of course)

The bonkers thing is that all of the visualizations show basically all of the terms pretty close to the middle on a log odds scale. If "highly unlikely" means 10-20%, how do you express 1 in 10,000??

I think it's been established that cautionary tales don't work. ("Tech Company: At long last we have created the Torment Nexus from classic sci-fi novel Don't Create the Torment Nexus") So we might as well have some positive visions of the future! They might be more pleasant to read about too.

Games drawn from this uniform distribution can't even be implemented in our physical universe (you would need exponentially large lookup tables to store the rules). There is no chance of ever encountering any of them.

Of course, there are "games" like "invert sha-512" that can be implemented in our world but are probably impractical to learn. But NFL has nothing to say about them; a game that simple has zero measure in a uniform distribution over problems.

A start might be to enforce, or perhaps strengthen, laws against false advertising. I think most advertising is dishonest outright or at least by implication or omission. If everyone in the chain of custody of commercial speech was held liable if the speech was misleading, the world would look rather different. Compare the tone of a company's ads to the tone of its SEC filings.

This typechecks:

    function prove_anything<P>(){
        function prove_false() : False {
            return prove_false()
        }
        let f = prove_false()
        return contradiction<P>()(f)
    }

I think a proof assistant will usually have a total notion of computation to avoid this kind of circular proof. And there are probably some subtler unsoundnesses in TS to worry about.

(I'm not any kind of expert in this area. It's possible the original author intends that you execute the proof function as well as typechecking it, which I guess will prove termination, although I think for many proofs you might run out of resources trying to do that, and it's probably still not sound.)

> The key point is that a government that issues debt in its own currency can always service that debt, and this is NOT inflationary.

Hmm. Let's follow your argument to its conclusion. Why stop at 300% of GDP? Why stop at 300 times GDP? It seems that even a small nation with a sovereign currency can eliminate all taxation, borrow an infinite amount of money, buy an infinite amount of stuff, make all of its citizens infinitely wealthy, service its debt with printed money forever, and prices and interest rates will both be unaffected. It's amazing, then, that no nation has yet taken advantage of this exploit!

I feel confident that is not right. I think it may be right that (marginally?) there is not a big difference whether a fixed amount of government spending is financed by taxation or debt, because printed dollars and t bills are so easily interchangeable. But it seems that you are trying to use this argument to prove that if these things are equivalent that they are (in any quantity!) harmless, and that's a non sequitur.

There is some overlap, but the situation in a hypervisor is in fact pretty different.

Containers are doing two jobs for us: they give our customers a convenient way to send us software to run, and they give us a convenient place to simulate the network boundary between different machines in a distributed system. The whole guest operating system running the containers is also running inside the deterministic hypervisor and under test (and it's mostly just NixOS Linux, not something weird that we wrote).

I'm a co-founder of Antithesis.

In the specific case in question, the biggest problem was that dependencies like Zookeeper weren't compatible with our testing approach, so we couldn't do true end to end tests unless we replaced them. One of the nice things about Antithesis is that because our approach to deterministic simulation is at the whole system level, we can do it against real dependencies if you can install them.

I was a co-founder of both FoundationDB and Antithesis.

There's indeed a connection between record/replay and deterministic execution, but there's a difference worth mentioning, too. Both can tell you about the past, but only deterministic execution can tell you about alternate histories. And that's very valuable both for bug search (fuzzing works better) and for debugging (see for example the graphs where we show when a bug became likely to occur, seconds before it actually occurred).

(Also, you won't be able to usefully record a hypervisor with jockey or rr, because those operate in userspace and the actual execution of guest code does not. You could probably record software cpu execution with qemu, but it would be slow)

I'm a co-founder of Antithesis.

Couldn't you just continue to serve the tiny .narinfo files from a trusted central source while letting bittorrent or ipfs cache the .nar files (big, but can be validated by hash)? It doesn't allow for untrusted builds but it would work with all kinds of derivations.

In principle, signatures also address the cache itself being untrustworthy, right?

A program can only halt once, but can beep any number of times. So you can make a size X program (or turing machine) that simulates running every program (or turing machine) up to some size Y >> X, and whenever any of those programs halts it beeps. The last time it beeps will be when it simulates the halting of BB(Y) after more than BB(Y) steps, so BBB(X) > BB(Y) >> BB(X).

IIRC basically this same construction means that while knowing BB(N) lets you (very slowly) compute the halting problem for programs up to size N, knowing BBB(N) lets you (even more slowly) compute the halting problem for turing machines supplied with a halting oracle up to that size.

It only takes a few v4 addresses to make enough v6 addresses for everyone, so there is no long term rent once all edge devices are v6. v4 addresses being temporarily "rentable" helps push the system towards that end goal (because the key is to fix the edges, and the edges are the ones getting screwed paying for v4 addresses if they want them). It doesn't matter if major interconnects upgrade - if they want to shuffle v4 packets tunneling v6 packets, and have enough addresses to do it, it's their problem.

I still think there are technical flaws in my proposal - for example, probably the tunnel should use udp so that it can traverse totally clueless NAT - but I think the basic idea of trying to upgrade the edges while fully interoperating is incentive compatible in a way that the idealistic v6 approach just isn't.

The key point is that all v6 addresses are owned by v4 addresses and therefore tunnelable, and that tunneling support is mandatory. There is no external prereq to having an individual device be able to open connections to v6 addresses, and only support at the router (with a public address) is needed to receive connections from any v6 address.

There is no way around upgrading end devices. But the problem with v6 adoption isn't the number of end devices from before 1995.

Basically the adoption plan could have been:

1. Get end OSs to have v6 support. They gain the ability to make outgoing connections to v6 addresses right away. There's no reason, from the beginning, for this not to be enabled by default with zero configuration from the beginning.

2. Get NAT routers at the edge to have v6 support. Gains the ability to publish services from inside without awkward port forwarding etc (and increases the benefit of 1)

3. Slowly make v4 addresses expensive so that consumers make do with less than a /32. They need v6 capable endpoints but can communicate as clients with anyone, and as servers with anyone who has adopted v6

4. Eventually v4 addresses are so expensive, and the number of machines running browsers that don't support v6 so small, that small time web sites stop taking a /32

etc. it doesn't really matter when the network backbones upgrade, it just saves a few bytes on the wire and they internalize the cost of that

This just doesn't seem like what happened in our timeline.

Assign 2^96 addresses to each IPv4 address. The original address is now a.b.c.d.0 and there are lots more a.b.c.d.x. When sending a packet over an IPv4 link, translate packets with .0 destinations to v4 packets and embed others in a special v4 protocol. When receiving a packet do the reverse. Now you need a v4/.0 address only if you are directly connected to a v4 peer, and an upgrade is useful even for a single computer behind a NAT.

I came up with this idea in like 5 minutes so I'm sure it is flawed. But i think that if we had a realistic design we could have been done with the transition in early 00s.

> You may make production use of the Licensed Work, provided such use does not include offering the Licensed Work to third parties on a hosted or embedded basis which is competitive with HashiCorp's products.

Having your use of something important hinge on this one awkward sentence seems kind of scary. It's unclear to me whether, if you use (say) terraform for production infra, and someday HashiCorp releases a new product competitive with yours or merges with your competitor, your use of TF is then in violation of the license. "Offering the Work" is not defined and seems like it could be interpreted in different ways.

It's apparently hard to measure zero vs extremely low resistance with the two probe setup you are imagining (I guess because the probes and wires aren't superconducting, so most of the resistance in the circuit is not in the sample). The graphs I have seen are all made with a four probe setup [1], where a constant current is run through the outer probe pair and the voltage across the inner pair is measured. If the inner probes have contact issues, the voltage (and inferred resistance) drops, potentially to zero.

[1] https://www.ni.com/docs/en-US/bundle/ni-daqmx/page/measfunds...

I think I can solve your puzzle.

First assign the number of potential aunts and nephews in each continent, city, etc top down in your tree (ensuring that the numbers are equal at the top and that you can reversibly assign a compact integer to each aunt and to each nephew). Then you need an invertible pseudorandom permutation of the right size P, i.e P(P^-1(x))=x for 0<=x<N. For nephew n the aunt is a=P(n) and you can walk down the tree to generate the details of the entity which is aunt a. If you start with the aunt you just use P^-1.

Cryptography has already developed families of functions P. For N=2^128, AES is such a family. For non power of two N, you want to look at "format-preserving encryption". For example you can use a Feistel network to permute the next larger power of two and simply iterate that permutation until you get a result in range.

I think you could extend this primitive to nonuniform graphs (aunt more likely in the same city) and more kinds of relationships. You can also use rejection sampling to condition the relationships further and probably to deal with the top down population assignment being approximate.

All that said, I think procedural generation currently runs out of creativity long before you would run out of memory to store explicit relationship indices. I think it's a lot more hopeful to get more creativity out of generative AI while keeping things grounded by explicitly representing the world, even if it "doesn't scale" to creating trillions of galaxies.

The punchline of the story is supposed to be that Gates just knows that if the world's most famous investor proposes a bet, you don't want to take the other side of it. If Buffett wants to go second, then so does Gates.

Instead of reading this article, you can just read "The Peace of Dives" by Kipling... and then look at its publication date.

Sounds like the POTAXOR strategy [1].

[1] https://slatestarcodex.com/2014/06/15/fish-now-by-prescripti...

It's possible to take anything good to excess. For every piece of advice, someone probably needs to hear the opposite.

But... if your manager is displeased with most ICs for brainstorming, considering edge cases, researching possible solutions, refactoring, helping other people, testing, and automating... you should probably consider working somewhere else. These are all things the industry does too little of, and that my company puts significant effort into encouraging and rewarding. They are also important steps in growing into (technical or people) leadership roles. And they are nowhere near the top of the list of things that people waste time on.