If they reject more ads they get less money.
For small separate changes in isolation then maybe it's ok? But not for whole days 8 hours each. But then you need to watch for bugs coming from interaction with previous changes and in 700k loc that might be…
Soundness bugs in lean are not unheard of. That's why they recommend using external checkers for "malicious" proofs. https://github.com/leanprover/lean4/issues/14576
To be a slightly more neutral It'd be a nice opportunity to base it on esperanto.
Pretty cool, especially in finite fields. Though coefficients seem to blow up pretty quick in Q?
Technology depends on a lot of people cooperating around the globe. Disrupt a few critical chains (power generation, fertilizers, computers), add a bit of good old war and you'll soon be in the era before Haber process…
I like the concept of separation logic as much as the next guy, but I don't think this is it. Just look at the examples, with loop invariants alone being longer than the whole example. It's not only a problem with…
> To meet and spend time with other human beings. The design is very human.
Yes > Rather, the remedy for Plaintiffs’ injuries lies in pursuing tort claims, electing representatives who will better manage the public-water system, and petitioning their representatives for other remedies. which is…
On the other hand it means that states can just not do that and leave their citizens without clean drinking water.
Per https://en.wikipedia.org/wiki/Peano_axioms#Set-theoretic_mod... > The Peano axioms can be derived from set theoretic constructions of the natural numbers and axioms of set theory such as ZF.[15] If you're going…
You make relations and functions out of sets and prove theorems about them, reducing definition of things in terms of belonging to a set. This isn't particularly complicated.
It's the same way you don't need to have GCD in stdlib to say that you can compute GCD in C++. You can make your own using parts given. You don't need to add any axioms, you just build some sets to represent numbers and…
> Moreover, Robinson arithmetic can be interpreted in general set theory, a small fragment of ZFC. https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t...
Or you could wait a day or two to write about it, but with initial reactions etc. added. 24-hour new cycle came into view in 80s I think?
If this anything like CERN detectors, they get amounts of data so vast that they have to discard almost all of it to be even able to record it. Depending on heurestics you use to discard data you might be discarding…
I still remember getting support mail every time Apple released an OS update. For a week or two there'd be reports of things crashing randomly with stacktraces that didn't seem to make much sense. One of reasons why I…
I can imagine them not having a lot to do during winter nights, besides sitting by the fire. That's a lot of time for carving.
I think the core of this is google vs oracle case. I think they'll be in the clear unless they hit some specific (design?) patents.
I've used docker until recently just because it was what I was used to. It turned out I can basically just `apt install podman` and it'll just work. I might have stayed a bit behind the times with having podman slotted…
I wish it was just users. I once had to explain to a PM on client's side for 10 minutes that no, the software can't split $1.00 into three exactly equal invoices and we need to put that remaining $0.01 somewhere. In the…
With the size of these matrices I don't think they are even meaningfully colocated with themselves in memory. You'll end up with some dataflow TPU architecture anyway because you'll have to stream the second matrix to…
What are you talking about? There's a lot of expressions like O(n + k), O(n * k) or O(n * log k) in typical algorithm books (CLRS certainly has them). There's nothing special about O(n - k).
It has two parameters and depending on their relation it will act differently, it's reasonable to include this information. It is worst case O(1) when n and k don't differ much.
If k = n - constant it comes out to O(1).
If they reject more ads they get less money.
For small separate changes in isolation then maybe it's ok? But not for whole days 8 hours each. But then you need to watch for bugs coming from interaction with previous changes and in 700k loc that might be…
Soundness bugs in lean are not unheard of. That's why they recommend using external checkers for "malicious" proofs. https://github.com/leanprover/lean4/issues/14576
To be a slightly more neutral It'd be a nice opportunity to base it on esperanto.
Pretty cool, especially in finite fields. Though coefficients seem to blow up pretty quick in Q?
Technology depends on a lot of people cooperating around the globe. Disrupt a few critical chains (power generation, fertilizers, computers), add a bit of good old war and you'll soon be in the era before Haber process…
I like the concept of separation logic as much as the next guy, but I don't think this is it. Just look at the examples, with loop invariants alone being longer than the whole example. It's not only a problem with…
> To meet and spend time with other human beings. The design is very human.
Yes > Rather, the remedy for Plaintiffs’ injuries lies in pursuing tort claims, electing representatives who will better manage the public-water system, and petitioning their representatives for other remedies. which is…
On the other hand it means that states can just not do that and leave their citizens without clean drinking water.
Per https://en.wikipedia.org/wiki/Peano_axioms#Set-theoretic_mod... > The Peano axioms can be derived from set theoretic constructions of the natural numbers and axioms of set theory such as ZF.[15] If you're going…
You make relations and functions out of sets and prove theorems about them, reducing definition of things in terms of belonging to a set. This isn't particularly complicated.
It's the same way you don't need to have GCD in stdlib to say that you can compute GCD in C++. You can make your own using parts given. You don't need to add any axioms, you just build some sets to represent numbers and…
> Moreover, Robinson arithmetic can be interpreted in general set theory, a small fragment of ZFC. https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t...
Or you could wait a day or two to write about it, but with initial reactions etc. added. 24-hour new cycle came into view in 80s I think?
If this anything like CERN detectors, they get amounts of data so vast that they have to discard almost all of it to be even able to record it. Depending on heurestics you use to discard data you might be discarding…
I still remember getting support mail every time Apple released an OS update. For a week or two there'd be reports of things crashing randomly with stacktraces that didn't seem to make much sense. One of reasons why I…
I can imagine them not having a lot to do during winter nights, besides sitting by the fire. That's a lot of time for carving.
I think the core of this is google vs oracle case. I think they'll be in the clear unless they hit some specific (design?) patents.
I've used docker until recently just because it was what I was used to. It turned out I can basically just `apt install podman` and it'll just work. I might have stayed a bit behind the times with having podman slotted…
I wish it was just users. I once had to explain to a PM on client's side for 10 minutes that no, the software can't split $1.00 into three exactly equal invoices and we need to put that remaining $0.01 somewhere. In the…
With the size of these matrices I don't think they are even meaningfully colocated with themselves in memory. You'll end up with some dataflow TPU architecture anyway because you'll have to stream the second matrix to…
What are you talking about? There's a lot of expressions like O(n + k), O(n * k) or O(n * log k) in typical algorithm books (CLRS certainly has them). There's nothing special about O(n - k).
It has two parameters and depending on their relation it will act differently, it's reasonable to include this information. It is worst case O(1) when n and k don't differ much.
If k = n - constant it comes out to O(1).