u/SkiFire13

That's not a valid excuse. If I have to use an LLM to summarize your very verbose paper then you should have done that summary yourself before publishing it. And is assuming your paper is even worth reading, I could just ask my LLM to research the same data if needed.

You could use a indexmap::IndexMap, then get the index of elements and from there it's as if you were working with a Vec/slice.

The compiler splits the work in multiple codegen units. Each codegen unit can ran in parallel and thus can be faster, moreover it can also help with incremental compilation. However as a consequence of this each codegen unit can end up seeing the constant, evaluate it, and include its result in the final binary. Each codegen unit only evaluates it once, even if it's used more than once, but different codegen unit won't coordinate.

how parallelizable is this?

This doesn't answer your question but you likely don't want to parallelize within the algorithm, instead you want to run the algorithm over many functions in parallel.

vulnerabilità trovata dentro un programma di bug bounty o su una tua installazione in locale o dentro un contesto di PT che il proprietario dell’infrastruttura ti aveva autorizzato non verrai mai denunciato

Quindi se un'azienda ha un sito o servizio online con nessun programma di bug bounty/PT e tu noti una banalissima vulnerabilità in esso, non ti è permesso legalmente di riportarla all'azienda o ad un ente statale.

Basta non riportarla e non verrai denunciato, ma la vulnerabilità rimarrà lì, insomma tutto funziona come dovrebbe.

Not even overly restrictive, some code might hit this bug and break Rust's rules without actually doing anything unsound with it, for example the code might not exploit the 'static bound in drop, even though the data there is not 'static.

After all we have seen I doubt they will stick to that rule. They will most likely end up with something that requires more annotations than Rust but they will claim the annotations won't be needed in practice and thus are not "viral", all while likely having some issues that will require a lot of opt-outs for code that won't be checkable.

Makes sense, thanks!

some code was previously using some unsupported hacks to refer to this never type on stable rust, and will be broken by the fact that the Infallible type will become an alias for the never type

Is this actually the case? From what I see the code that will break due to Infallible becoming an alias will be code like use std::convert::Infallible::{self};.

The hack used to refer to it should continue working because it doesn't actually depend on the never or Infallible types, it's just a way to refer to the return type of a function.

AI can formalize Wiles’ FLT proof

The work for formalizing that proof already started years before LLM became popular. The types were already there, written by humans, while the AI produced the proof terms based on the already existing proof by Wiles.

Even if it the LLM translated the theorem statement (i.e. the types), it would not be an indication that it will also faithfully translate your English "spec", since Fermat's Last Theorem statement is way simplier than any program spec you could think of.

I will still review

I think you're underestimating the amount of code needed for these proofs, and hence how much work you'll have to do reviewing them.

why should I need to remember minor details of the syntax?

How do you plan to review without remembering that?

I mean if AI is not going to help with the difficult parts at all then these languages will remain obscure.

Declaring the types is the easy part. It's like stating a theorem. Finding a term for that type (i.e. finding the proof) is the hard part, but finding it can be the AI job and you don't have to review that part, because the language make sure that it will satisfy the type you have written.

Not all issues/bugs are the same. I have also seen AI going in circles, creating a bug when fixing another one, then effectively reverting the change to fix the new bug and so on.

behind the scenes I actually do a lot of testing making deliberate mistakes to see if my borrow checker would catch those mistakes

That's nice! But testing is not a proof of correctness, and it only covers the cases that you could think of. In comparison Rust got a whole machine-checked proof that the base concepts of the borrow checker are sound https://plv.mpi-sws.org/rustbelt/popl18/

I liked the post, but I would a more formal explanations of the rules of the new constructs that Zeta allows, follow by some sort of intuition for a proof of why those rules are ok. In its current form the post mostly contains examples for the "good path", but those don't give intuitions for why the language would work in weird situations.

Can we please be clear: Making any observable change to the code is a semver hazard.

And so? Not all semver hazards are the same, some carry more risk than the others.

if the ambition is to prevent them at all costs, even holding back legitimately useful language features that the people want.

What makes you think that's the ambition? I just gave you an example where the exact opposite choice was made.

Preventing people from doing something interesting because they may have accidents is far too conservative.

Rust has made choices in the past where convenience won over semver hazards (see e.g. autotraits), but that needs to be proven the best/only way, and right now I think they're exploring alternative solutions. Moreover the existance of the macroless features shows that they care about the UX here, and that if there's no reasonable alternative solution, or if the semver footguns ends up being not too bad, they might go for the implicit solution.

It will break a lot of users and make the interface harder to use for anyone that doesn't need io-uring. For tokio this will mean in particular having a 2.0 release.

MTE works by having the allocator set a tag to a region of memory, and then returning pointers whose high bits contain that tag. Access to that region of memory needs to be performed using pointers having the correct tag in the high bits, otherwise you'll get an interrupt (generally then transformed into a SIGSEV). This generally conflicts with libraries that expect the top bits of pointers to contain only zeros and try to use them for other kind of tags.

I agree, not everything should be considered for semver compatibility.

However we also need to consider how likely it is to make a semver breaking change and how likely it is going to break downstream dependents. If it's likely to break downstream dependents and easy to involuntarily make then that becomes a problem.

The problem is that the compiler is a bit too strict when it comes to symbolic equality, and rejects 1 + N == N + 1 since the symbols are swapped.

If you want to allow that then you open a can of worms because where do you draw the line for when some equality operation is accepted or not, and how do you make sure that you can evolve the compiler without breaking backward compatibility in this area?

basic arithmetic rules

Depending on your arithmetic foundation (e.g. using Peano axioms) then 1 + N == N + 1 can be theorem, not a basic rule.

The only similar thing I've worked with in the past was this really simple pure C graphics library where I'd make a window and then draw pixels to it by coördinates

And did you understand how those worked? What is the level of understanding you're looking for here?

Does this work with ARM MTE (Memory Tagging Extension)? I suppose that your library works by embedding some kind of tag in the heap pointer in order to distinguish between pointer and a 8-bytes string, and to do that it must assume that part of the pointer will have a given fixed value (e.g. 0), but AFAIK MTE breaks this assumption of yours.

I think the fundamental issue is that the compiler wants to use symbolic equality for type checking const generics because it can work when the const generic value depends on some other generic value. However in some cases this can unexpectedly return false negatives, and the rules for this are pretty awkward and unintuitive. gca! basically forces the subset of expressions where the rules are predictable.

Your example for semver stability applies to the current stable as well, but I do agree that semver is also a pretty big issue here. Without gca! it becomes easy to update your code to no longer work due to those unintuitive rules.

One expands to the literal true/false, while the other decides whether to include the tokens following it.

The if works at the language level: it decides which code runs or not, but it has to be valid code.

The #[cfg(...)] works at the parser level: it decides which tokens the compiler will even look at.

The standard IO traits doesn't support async IO (well, you can have read/write return a WouldBlock error, but that's not IO uring and you have no "notification" mechanism, so I don't consider that proper async IO).

Pretty much all ecosystem crates of the early days (that coincidentally are also the most popular ones) have IO traits that are incompatible with IO uring, precisely because they aren't structured as async fn read(buf: Buf) -> (Buf, Result). Just to name a few: tokio, async-std, futures-io, async-io (used by smol)

I mean that people manually boxed large variants of enums used in the implementation of rustc itself.