def function_spec bleh blah := math_blargh
    def function_impl bleh blah := code_blargh
    theorem function_correct: forall bleh blah, function_impl bleh blah = function_spec bleh blah := by { long proof }

Maintenance is still a headache. If you change a small piece of your code, you would then need to change all the proofs that refer to it, and then if the specs also changed then you need to change all proofs that refer to those specs, etc.

If digit i has significance b^i, then b (the base of the exponentiation) is the base (or radix) of the number system.

The page you linked explicitly mentions the binary version of Booth encoding as having base b=2 and three signed digits {-1, 0, 1}. The quaternary version similarly has b=4 and five signed digits {-2, -1, 0, 1, 2} ... and possibly sometimes -0 in practice, not sure.

Edited to add: I'm also not sure whether real-life implementations have -0 as an option. Of course -0 could be normalized to +0, but it might be cheaper not to bother if the sign is applied after the digit selection.

Adds are not really considered negligible; the article is just sloppy. (Some shifts might be negligible in some models because a fixed shift requires no logic gates.) The cost of the adds in Karatsuba is significant both theoretically and in practice, and determines the cutoff where Karatsuba is useful. But the exponent in O(n^(log_2 3)) is dominated by the recursive multiplications; the adds only affect the leading constant hidden in the O().

There's also NTT / Fourier multiplication as an option, for big integers or polynomials or modular arithmetic.

Then for each digit, you select between the other input multiplied by 0 (all zeros), +1 (identity), +2 (shift left by one bit), or -1 or -2 (flip all the bits of +1 or +2, plus a correction). Since a number has about half as many digits in base 4 as in base 2, you have about half as many digits to sum as if you'd done this in base 2.

Then you sum up all those results, but since carry propagation is expensive, you mostly use "compressors", e.g. you sum up three intermediates at a time, but you do it bit-by-bit, where three 1-bit numbers add up to a 2-bit number (from 0 to 3). This is called a Wallace Tree. The point is that you are generating carries, but you aren't propagating them, just adding them back into the set of things to be summed.

At the end of the tree step, you have just two numbers left, and you add them conventionally. That's the only step that needs full carry propagation.

If you are implementing a multiply-add, or multiplying several numbers and adding up all the results or similar, then you usually only need one full carry propagation stage.

The overall circuit has quadratic area but only a logarithmic depth in gates. IIRC whether to do Booth or not is a tradeoff: at least in some circumstances the rewrite steps make it slower but smaller. Hardware tool vendors have done a lot of work to tune these circuits very tightly, using e.g. specialized gates like AOI, heuristics for how to set up the tree, etc.

There are different definitions of "zk", of "proof". Eg do "proofs" of false statements not exist, or are they just hard to find? If they exist but are hard to find, then it's often called an "argument" instead, which is the "AR" in zk-SNARKs and zk-STARKs.

One common definition of zero-knowledge protocols is that you can make an efficient simulator that makes convincing transcripts of the protocol without knowing the relevant secret (up to and including whether the statement to be proved/argued is even true). For interactive proofs, the simulator is usually supposed to output a transcript of the messages sent between the prover and the verifier, and the trick to making the simulator work is to choose later messages before earlier ones (e.g. challenges before commitments). But in non-interactive proofs, there's only one message, so that trick doesn't work and the simulator would have to output the proof itself.

The Goldreich-Oren result shows that this definition of ZK conflicts with soundness, unless the type of problem you're doing ZK proofs for was easy to begin with. IIUC this is for a simple reason: if a simulator can efficiently output a convincing proof of any true statement of the type your zk proof system covers (this is the zero-knowledge property); and if for false statements there is no proof that will convince the verifier (soundness); then you have an efficient algorithm for checking whether the statement is true or not, which is just to check whether your simulator convinces the verifier. This means that the underlying problem is by definition easy, so there's not much point to having zk proofs for it.

Goldreich-Oren doesn't apply to zk-SNARKs or zk-STARKs, because they are not perfectly sound, and in particular because you can get around the impossibility using the trusted setup in zk-SNARKs (essentially a secret key that lets you efficiently prove false statements) and/or by messing around with the random oracle model (pretend that the hash functions are replaced by magic, and then let the simulator tinker with that magic). Also zk-S?ARKs are arguments of knowledge (not just e.g. "a discrete log of this point exists" but "the prover knows the discrete log") which also changes the model.

As I understand it, the new result is basically to make your proof a NIWI-proof ("Non-Interactive Witness Indistinguishable proof", a weaker notion of zk-proof) that:

* Either [real statement you're trying to prove]

* or else [false statement that's almost impossible to prove false], e.g. "there are contradictions in your axiom system".

Such a proof can be made perfectly sound, since NIWI can be perfectly sound, and the second half is supposed to be false. There's no simulator, but if the false statement were true then there would be a simulator, where you always feed the NIWI eg a contradiction in the axiom system, instead of a proof of the real statement. (The definition of NIWI is that it should be hard to distinguish the proof resulting from these two cases.) The new paper also argues that this result, where there's no simulator but it's hard to prove that there's no simulator, is almost as good as the simulator actually existing.

Probably in practice you wouldn't do this, but you would instead try to make sure that a zk-SNARK, zk-STARK, NIWI etc is good enough in your use case.

For cancer in particular, pharmas don't (and mostly can't) just target a drug to chronically treat some cancer over the long term but not cure it. Instead they pick some target that's believed to contribute to development (/ metastasis / treatment resistance / whatever) in whatever cancer, and make a drug to interfere with it or to target an immune response to cells that make it. If it's stable, nontoxic, and looks potentially effective enough they'll take it to clinical trials. During clinical trials they'll find out whether it does nothing, gives you a few extra months, or has a chance at curing the disease. Usually the answer is that it does nothing or almost nothing, or isn't worth the side effects, and then the company wasted its time and money. Drugs with a chance to cure common types of cancer can be enormous successes -- see eg Herceptin.

Cancers are difficult diseases and it's rare to find something that reliably cures them. But drug companies aren't pulling their punches. Like they would never say "oh this drug clears breast cancer too reliably, we should make it less effective so that people will be more likely to die but also might take it for longer".

They do claim it at least for iPhone 15 "under ideal conditions": https://support.apple.com/en-us/101575

Edited to add: Sieving has got to be much faster than M-R if you want all primes of a certain size. You would use M-R or Baillie-PSW if you are testing them one at a time.

But sure, there are other shipyards they cleaned up in less than three decades.

And OK, sure, there's a lot of industry that ought to happen somewhere. Someone has to build ships and electronics and whatever, and if California's code is too strict then it just becomes NIMBYism. But if some company moves their gigafactory to Reno for easier permitting, I don't whether (or more likely by how much) CA is too strict, or NV is too lax. And I know that CA has NIMBYish and overregulatory tendencies, but given the clear bullshit on this website, I'm not inclined to give it the benefit of the doubt either.

I'm especially doubtful when it says "THE classic example of what you can't do in CA" is auto paint shops ("Impossible"!) ... but then the detail it gives is that they're "effectively impossible" to permit in the Bay Area AQMD, that being only one of the state's 35 AQMDs (albeit one of the larger ones).

On languages other than English: in general, different languages do word division very differently. At least in German and Dutch, many of those phrasal verbs are separable, meaning that they are one word in the infinitive but are multiple words in the present tense. So for example, where in English you would say "I log in to the website", in Dutch it would be "Ik log in op de website". "Log in" is two words in both cases, but in Dutch it's the separated form of the single-word separable verb inloggen ("I must log in now" = "Ik moet nu inloggen"). The verb is indeed separable in that the two words often don't end up next to each other: "I log in quickly" = "Ik log snel in".

Dutch, like German, has lots of compounds. But there are also agglutinative languages, which have even more complex compound words, perhaps comprising a whole sentence in another language. Eg (from Wikipedia) Turkish "evlerinizdenmiş" = "(he/she/it) was (apparently/said to be) from your houses" or Plains Cree "paehtāwāēwesew" = "he is heard by higher powers"; and these aren't corner cases, that's how the language works.

I got one with low-force switches. It's very comfortable to type on, but between the low-force switches and slightly different layout from a regular keyboard (column-staggered, concave, symbols in different locations) I make more mistakes. So I usually type on my laptop instead, especially while coding.

My phrase "how economists expect you to set it" is probably wrong here, since I'm not an economist, I've just read the most basic theory about how to use this tool, and also used it myself (on eBay, you know, years ago when the site was mostly auctions). So I don't really know what "economists expect", but rather the basic guidelines for using this tool. You got me there.

> I think this is the problem. When most sciences observe reality diverge from the model, they see that as a flaw in the model. When economists (at least you HN "economists") observe reality diverge from the model, they seem to see that as a flaw in reality.

But like, to double-check here: "reality" means your imagined use of a tool that you do not in fact use, right? Like you say you "don't do auctions" and I'm trying to explain what that option is for, and you're countering that the basic "how to use this tool" explanation is a wrong model of reality?

That said, the max price is supposed to be a price where you are not especially happy to get the item at that price, but not really sad either, a price where you would say "well, I hoped for better but I guess that's a fair deal". That's not realistically pinned down to the cent. But if you set a max price at $5000 and would be happy to get the item at $5000.02 (for some reason other than satisfaction from sniping), then you set your max price wrong, or at least differently from how economists expect you to set it.

For tricky-to-price items like unique art pieces, the idea that you can pin this down might be a fantasy, but for commodity items it's pretty reasonable. If you can buy the same thing at costco dot com for $500, then it's probably not worth more than $500 to you, and if at auction you get outbid and it sells for $500.01 then you'll shrug and go order the same thing for a cent less, having wasted only a few minutes of your time. If the item you're bidding on is discontinued (e.g. it's last year's model) but you can buy a slightly better one for $550, and you can spare that extra $50, then again you won't be too sad about getting outbid. Online auctions are more popular for used items, but again in that case you usually still have an idea of what a used item is worth to you.