Jweb_Guru

Yes, but unlike most of the proposed solutions to this problem, this one was (1) seriously considered prior to the release of Rust 1.0, and (2) wouldn't have caused major changes to the way most people write Rust programs in practice. i.e. Rust without panic catching in safe code is still essentially Rust.

`.clone()` is usually implemented in terms of `Copy`, but the real problem that I don't know how to solve without `Copy` is the use of references. Every time you call a function on a shared reference (including the one used by `clone`) you are implicitly copying the reference. It only works because of `Copy`. Without it, I think you would need unsafe code or something in order to call a shared method and retain access to the original reference, which would pretty much no longer be Rust since the vast majority of methods wouldn't be correctly expressible in the safe subset. There might be reborrowing style tricks you could use to get around this, but as you said the "core" of Rust shouldn't have reborrowing. Or maybe you could implement clone on references in unsafe code and then just explicitly take a reference to the reference every time you needed to duplicate it... There is also the linear type trick you can use to copy a value by pattern matching it destructively, explicitly enumerating all possibilities, and then generating a fresh product with each possibility listed twice, but that cannot implement copy for references.

In any case, I think it's just true that `Copy` is quite fundamental to Rust. IMO even if you could somehow turn all instances of it into syntactic sugar (which I think is not true, as the `Cell` example shows), the surface language you used would be sufficiently unlike Rust that it wouldn't really be Rust anymore.

I think a version of Rust in which catching panics is unsafe would be entirely justifiable and probably should have been more strongly considered.

I'm actually unconvinced you could do without `Copy`. It's both in the core of the language and essentially required for stuff like shared references to work correctly. Copying could be replaced by a keyword instead of happening implicitly, but that's different from removing the concept entirely from Rust.

The rest, sure, you could do without (reborrowing can't be emulated but I don't think it's strictly necessary to write real code). I'd add catchable exceptions and the use of traits instead of explicit modules as things that I think tremendously complicate the language semantics and are almost certainly not strictly necessary to achieve Rust's language goals.

Yeah embassy has improved tons recently. This is because embedded Rust is receiving a lot of investment from industry, embedded engineers desperately want a real C alternative there.

RocksDB diverged from LevelDB a long time ago at this point and has had extensive work done on it by both industry and academia. It's not a toy database like LevelDB was. I can't speak to the problems they're supposedly hiding in their stack, but they are unlikely to come from RocksDB.

C also has lots of undefined behavior that lets compilers make assumptions they have a very hard time proving in safe languages. C++ takes this even further with stuff like TBAA. Sure it doesn't give the compiler as much to work with as something like Rust's pervasive restrict or Haskell's pervasive immutability, but on the other hand the compiler assuming things like "every array index is in bounds and infallible" exposes tons of opportunities for autovectorization etc. I think people overexaggerate how hard C is to optimize, at least compared to languages like Java and especially compared to languages like Ruby which let users do things like iterate through all the GC roots.

If you give the JIT compiler unlimited time with the code, then maybe. For real large applications, optimized JIT compiled code tends to lag behind AOT optimized C or Rust code, though I guess you could argue that these differences are language / runtime related rather than compiler related.

Mozilla spends very little on "hairebrained schemes" like (for example) Rust these days compared to direct investment in Firefox. Did you miss the massive layoffs that occurred many years ago?

Not a great analogy. CO2 emissions are a global phenomenon, so the average emission level is exactly what matters. Drunkenness is not.

Yeah it's not really "gaming" anything.

> Rust is rather heavy on its copy/clone imposed semantics making it potentially less suitable for low-latency or large data volume processing workloads. Picking Rust for its performance potential only means that you're going to have a harder time beating other native performance-oriented stream processing engines written in either C or C++, if that is your goal of course.

There is absolutely nothing in Rust's semantics preventing you from writing high-performance data processing workloads in it, and in fact it's one of the best languages for that purpose. Beyond that, the usual barrier to entry for working on a product like this written in C++ is incredibly high in part because stability and safety are so critical for these products--which is one of the reasons that in practice they are often written in memory safe languages, where C++ is not even an option. Have you worked on any nontrivial Rust data processing product where "copy/clone imposed semantics" somehow prevented you from getting big performance wins? I'd be very curious to hear about this if so.

> Google wasn't the first search engine but they were the best marketing google = search

Google's overwhelming victory in search had ~ nothing to do with marketing.

> Creating a thread is already very expensive, in a sane program your ten TLS constructors shouldn't come even close to the amount of bookkeeping that the kernel has to do to spin up a new thread.

This is not true, at least on Linux. With appropriate settings (e.g. a small stack) thread creation can be extremely cheap.

Yeah, this is a very strange article that completely contradicts its headline.

While it is true that not all distributions are normal, many distributions are approximately normal (or at least, normal in some sensible space that maps onto the actual collected data). IMO the amount of ink spilled on the idea that science is fundamentally flawed because distributions aren't always normal is probably too high (especially among non-statisticians), and frankly that's not where statistical analyses usually go wrong. A much larger problem (that has nothing to do with the ultimate shape of the distribution) is stuff like postselecting from a set of plausible models until you find one that finds significant results, and claiming that was what you intended to measure all along (this is why it's important to consider stuff like hyperpriors, much moreso than lack of normality).

Indeed, this conversation is a good illustration of the damage that Bayesian statistics have done to the "educated" populace. Not that they're inherently bad--it's just a different statistical approach, and it's generally good not to assume a universal background, that everything is normal, etc.--but by telling people it's fine to question statistical conclusions because the distribution might be different, it liberates certain people from ever having to actually change their minds based on new information, because they can just posit a different distribution that satisfies their own biases.

Yeah companies notoriously have to contribute back to the Linux kernel all the time, it is a massive success story for copyleft.

"Turing complete as long as you only use a polynomial number of steps in the size of the input" is another way of saying "not Turing complete" (doubly so when you look at the actual polynomials they're using). In fact, that paper just reaffirms that adding context doesn't improve formal expressive power all that much. And this is not equivalent to "well, Turing Machines are fake anyway because of finite space"--I can pretty trivially write programs in Coq, a total and terminating language, that will take far longer than the age of the universe to normalize but can be described in very little input.

It's code for "this is important and useful to the world, but probably won't lead to any immediately practical applications from the perspective of the funders (economically, militarily, etc.). But we have to say it might or we won't get funded."

Sure. Network switches for example have a pretty insatiable supply for processing speed.

> Basically I'm talking about the subset of proofs that could be done with pen and paper and pass a careful refereeing process. And you got that interpretation in your reply. You say that it is not insightful and that is of course an opinion you are entitled to.

Well, that part was me being subjective, but the objective part is that this subset of proofs doesn't necessarily have a verification algorithm "in NP." A very short proof that took time doubly exponential (in some sense) in the size of the proof could still feasibly be solved with pen and paper, because the proof was short even though the verification time was very long (or the verification was long due to a technicality--I describe an example below), depending on the exponent and the proof size. While at the same time, a short proof that took time polynomial (in some sense) in the size of the proof could take longer than the age of the universe to verify and be out of reach for both humans and computers, depending again on the degree of the polynomial and the proof size (and, since again proof verification in CiC is not reducible to 3SAT, proof search that incorporates non-polynomial functions plausibly might not even benefit from any speedup if P = NP!). I say "in some sense" because it's unclear exactly what function f to fix, since pretty much any decidable, total function you can think of grows more slowly than "max steps needed to typecheck a term of length n in CiC" (outside of other meta-level functions that similarly don't provide practical bounds on running time).

(To give a concrete example of where human verification might be much faster than computer verification of the same step, human mathematicians can easily use "tricks" when they know two results will be the same, without actually proving them equivalent, modifying the proof, or imparting extra knowledge to a verifier. For example, in Coq, by default you use Peano naturals, which are convenient for proofs but have very poor complexity--which means exponentiation actually takes exponential time to compute with them. Humans verifying a proof step will recognize this and just do exponentiation the normal way regardless of which inductive definition of naturals is being used, while for a computer to do so the person writing the proof has to deliberately switch out Peano naturals for digital naturals. It is entirely possible that the proof size when using non-Peano nats will be larger than the proof size using Peano nats, since induction on non-Peano nats is much more tedious, while the verification time is exponentially lower using non-Peano nats! So this is an example where proof search for a short proof and proof search for a fast to verify proof may be in conflict. It's also an example of somewhere where even though it's not explicitly stated in the proof, and even though different formulations of nats can't exactly be proved "fully equivalent" in CiC, humans verifying a proof understand that "in spirit" it doesn't really matter whether you use Peano nats or not.

Indeed, if you work with formal verification a lot, you will find you spend significant amounts of time optimizing your proofs, and learning tricks like whether to make an input to an inductive definition indexed or parametric, which are things that human mathematicians don't care about at all but which are very significant to the machine verifier).

In other words, I don't think being practical to verify can be described completely by either the complexity of verification or the size of the proof, and I don't think it's that useful to conflate this with a problem being in NP since (1) CiC proof synthesis isn't actually in NP, or even in the polynomial hierarchy, and (2) being in NP has a much more precise technical definition that only somewhat overlaps with "practical to verify."

> Let me put it this way: if you can write a paper with your proof and I can check it with only my brain without a computer helping me, then a poly time algorithm could also check that proof. Unless you believe something exotic about how the brain computes, how would it not be the case?

What does "without a computer" have to do with anything, and what do you mean by saying "in polynomial time" when restricted to a specific instance of the problem? To talk about solutions being checkable in polynomial time in the size of the input (which is what NP actually means, more or less, since every problem in NP can be encoded as a 3SAT formula with at most polynomial blowup), you have to actually specify some (infinite) class of problems first, otherwise "in polynomial time" doesn't really mean anything. Then, you have to specify a polynomial time verification algorithm for every instance in the class.

T he problem is that "proofs of length N" in CiC doesn't have a polynomial time verification algorithm (for checking proof correctness) in the size of the proof (and as I mentioned elsewhere, attempts to translate to an encoding that does can result in exponential or much worse blowup in the proof size, which does not allow you to put them in the same complexity class in this context). Moreover, it's very unclear how you'd even begin to carve out the complexity class of "proofs that can be verified quickly" because that pretty much requires you to write an algorithm to determine the complexity of the proof, which includes being able to determine the complexity of arbitrary functions in CiC (which as you can imagine, is not easy in such an expressive system! AFAIK, the totality proof requires axioms beyond ZFC, which means that the proof is not constructive and cannot provide any specific upper bound on the number of steps taken by an expression).

This means that there is no polynomial function f(n) such that a nondeterministic Turing Machine could always terminate after f(n) steps and (correctly) report "yes" when there is a proof with n or fewer steps and "no" otherwise, and it is rather unlikely that there is a decision procedure to restrict the proofs to "proofs that run in polynomial time in the size of the proof input" so you could practically apply your claim just to that subset of proofs (though I don't know whether the absence of such a decision procedure has actually been proven, but generally speaking problems like this are very rarely decidable for interesting programming languages like CiC, even if they are total). It does not mean that a human, or human with a computer, couldn't come up with a clever short proof in O(n) tokens that takes longer than f(n) steps to check on some particular instance of the problem for some particular f... because why would it?

I think what you're trying to say (to make your argument hopefully what you had in mind) is that if humans can verify a proof in "a reasonable amount of time", then a nondeterministic Turing Machine could produce the proof in "a reasonable amount of time." Which might well be true, but the point is that in CiC, how long the proof takes to verify has very little to do with the size of the proof, so this claim has nothing to do with proof verification being in P (and therefore, has nothing to do with proof search being in NP, which it isn't for CiC). More to the point, this is pretty much true of any problem of interest--if it takes more than a reasonable amount of time in practice to verify whether a solution is correct (where verification can include stuff like "I ran polynomial-time UNSAT on this instance of the problem" in a universe where P=NP), it isn't practically solvable, regardless of what fancy methods we used to arrive at the solution and regardless of the length of the solution. So I don't find this particularly insightful and don't think it says anything deep about humanity, mathematics, or the universe.

Anyway, I'm mostly just pointing out that even if P=NP, you can't really leverage that to discover whether a short proof exists in CiC in polynomial time. More concretely, there isn't an algorithm to convert an arbitrary CiC formula to a 3SAT formula without greater than polynomial size blowup (we know this because we can run non-elementary algorithms in CiC!). So even if we had a polynomial time 3SAT algorithm, which would solve a great many things, it wouldn't solve proof synthesis, which is another way to phrase "proof synthesis in CiC isn't in NP."

Reference for complexity: https://cs.stackexchange.com/questions/147849/what-is-the-ru....

> Can you claim that this equivalence proof is not in NP, without requiring this specific encoding? I would be very surprised to learn that there is no encoding where such proofs cannot be checked efficiently.

There are encodings where such proofs can be checked efficiently, such as the one that enumerates every step. Necessarily, however, transcribing the proof to such an encoding takes more than polynomial time to perform the conversion, so the problems aren't equivalent from a P vs. NP perspective (to see why this is important, note that there is a conversion from any 3SAT formula to DNF with a worst-case exponential size blowup, where the converted formula can be solved in LINEAR time! So the restriction to polynomial time convertible encodings is really really important in proofs of reductions in NP, and can't be glossed over to try to say two problems are the same in the context of NP-completeness).

> Therefore enumeration puts everything achievable by humans in the NP complexity.

This is a severe misunderstanding of NP. Hindley Milner type inference is worst case doubly exponential, for example, and we solve that all the time. We just happen to rarely hit the hard instances. I think the statement you're trying to make is something more along the lines of https://en.wikipedia.org/wiki/Skolem%27s_paradox, which is definitely fascinating but doesn't have much to do with P vs NP. Notably, this paradox does not apply to higher order logics like CiC with more than one universe, which lack countable models (which is why your intuitions about provability may not apply there).

I'm talking about the proof length, not the length of the proposition. In CiC, you can have proofs like (for example) "eq_refl : eq <some short term that takes a very long time to compute> <some other short term that takes a very long time to compute>" (where both terms can be guaranteed to terminate before you actually execute them, so this isn't semidecidable or anything, just really slow). In other words, there exist short correct proofs that are not polynomial time to verify (where "verify" is essentially the same as type checking). So "find a proof of length n for this proposition" is not a problem in NP. You can't just say "ah but proofs that long aren't meaningful in our universe" when the proof can be short.

> Math proofs are of NP complexity.

This is only true for very specific kinds of proofs, and doesn't apply to stuff that uses CiC like Lean 4. This is because many proof steps proceed by conversion, which can require running programs of extremely high complexity (much higher than exponential) in order to determine whether two terms are equal. If this weren't the case, it would be much much easier to prove things like termination of proof verification in CiC (which is considered a very difficult problem that requires appeal to large cardinal axioms!). There are formalisms where verifying each proof steps is much lower complexity, but these can be proven to have exponentially (or greater) longer proofs on some problems (whether these cases are relevant in practice is often debated, but I do think the amount of real mathematics that's been formalized in CiC-based provers suggests that the extra power can be useful).

> No, I am saying that is that it is easy to not verify something because you don't know the requirements up front.

Granted, but "this spec doesn't attempt to cover [X]" is very different from "this spec claims to cover [X] but actually doesn't, in ways the authors are unaware of." The former is quite common in formal specs with machine-verified correctness proofs and I've never heard anyone call that a "spec bug". The latter is not common in them at all. Perhaps you didn't intend this yourself, but the way people generally talk about "there could be a bug in the spec" is usually used to imply that the latter case happens often enough to make formal verification comparably effective to other defense mechanisms, when empirically formal verification is far, far more effective than any other bug prevention mechanism--to the point that people struggle to find even individual examples of these kinds of spec bugs.

> There are invariants which you can assume that are always true. If they aren't true for whatever reason you can abort and later track down what caused you to enter this state. It could be as simple as some logic bug or obscure as hardware malfunctioning and causing a bit flip (at scale you need to deal with hardware misbehaving).

Yes, and stating these invariants precisely is generally exactly what you need to do as part of writing the formal spec; getting them right is equally hard in both cases, so it seems weird to me to say that it's easier to check the invariants at runtime than to get the spec right. In fact, many formal specs have invariants that are exactly of the form "assert that if I ran this line of code, it would not throw an exception." Moreover, you can use much more "expensive" invariants when you're creating a spec, since you don't actually have to check them at runtime, which in practice lets you catch far more and more subtle bad states than you can with software checks. For example, your proof state can include a full history of every action taken by the application in any thread, and prove that invariants on them are maintained during every instruction, even when those instructions proceed concurrently and might witness partial or stale views of the latest values in memory; storing and checking all of this information on every step on an actual machine would be wholly impractical, even for high level languages and non-performance-critical software.

Obviously, things are defined according to some base model of the world, so if you are concerned about hardware bit flips (which in rare contexts you are) your spec should take that into account, but the vast majority of bugs in modern applications are not bugs of this form, and most defensive runtime checks are equally susceptible to hardware issues or other unexpected environment changes.

> Bugs are found in the process of testing too.

Yes, and I never said testing was bad. Formal verification and testing are complementary techniques, and tests are important in a formal verification context because you should be able to prove the tests will pass if you've gotten your spec right. However, them being complementary techniques doesn't mean that they are equally effective at reducing bugs.

Can you point me to some of the concrete bugs in formal specs with associated proofs that you are thinking of? Specifically in the part that was formally verified, not in a larger project that incorporates both verified and unverified components. Because my experience is that when asked to actually provide concrete examples of how formally verified code has bugs in practice, people find it quite difficult to do so. Formal verification is about as close to a silver bullet as it gets for eliminating bugs, even if it's not 100% (nothing is). It's certainly far better at eliminating bugs than vague philosophical positions like "making things safe by default" (what does that mean?) or "abort when you're in a bad state" (how do you know you're in a "bad" state? Isn't it in general at least as difficult as figuring out what the correct formal spec is? How easy is it to detect? Is the performance cost acceptable?).

In fact, what usually happens is the opposite of a formal proof being undermined by a bad spec--when an informal spec is formally verified, inconsistencies are often found in the original spec during the course of the proof process, and bugs are subsequently found in older implementations of that spec. Fixes are then incorporated into both the original spec and the existing implementations. Formal verification is a spec-hardening process.

This is true but mostly meaningless in practice. I have never found the people who say this every time formal verification comes up to be the same people who actually work in formal verification. The reality is that it's far far harder to mess up a formal spec that you actually have to prove a concrete instance of, than it is to mess up the code. With a buggy spec, in the course of trying to prove it you'll arrive at cases that seem nonsensical, or be unable to prove basic lemmas you'd expect to hold true. Formal spec bugs happen, but they're quite rare. Usually even when there are edge cases that aren't covered, they will be known by the authors of the spec due to the dynamics I mentioned earlier (cases encountered during the proof that are clearly being solved in ways that don't follow the "spirit" of the spec, only the letter). Of course, "informal" specs, or paper proofs, will have subtle bugs all the time, but that's not what we're talking about here.