kobebrookskC3

china seems to be doing fine. what are you gonna do, tariff the country that makes all your stuff? 100% tariff on iphones and macbooks?

> Constructing an invalid pointer in rust is UB

no, it is dereferencing, not constructing, an invalid pointer, that is UB. there is even a safe function provided to construct an invalid but non-null pointer: `https://doc.rust-lang.org/stable/std/ptr/fn.dangling.html`

is the fact that CHERI works better with C/C++ because of C/C++'s "anything goes" attitude, or simply that any hardware design that didn't support C/C++ well was discarded?

> simply by adding the formal verification that proves the safety which will work automatically

"simply" and "formal verification" are usually oxymorons, never mind "automatically"

i was responding this claim

> It would be perfectly possible to design a variant of Rust that gets you to 80-90% of Rust's usability, with the same safety, without macros.

i then present an api that i think relies on macros to expose a safe api

> Of course macros are good for encapsulation and abstraction, but that's a different subject.

no it's not. exposing safe abstractions is pretty much rust's raison d'être

but without macros, how would you expose a safe interface?

  fn pin(x: T) -> Pin<&mut T> { ... }

would move the value

no, you just missed my point. expanding the implementation is not a safe abstraction. show me how you'd implement the functionality of the pin macro as a safe abstraction.

yes, but the code inside is unsafe. the pin macro is like a safe function.

the macro uses unsafe inside, so that's another instance of unsafe you'll need to check, whereas the pin macro is like a safe function

how would you implement https://doc.rust-lang.org/stable/std/pin/macro.pin.html without macros? a macro is used to shadow the original variable so that you can't move it (safely) after you pin it

isn't that more like optimistic concurrency control?

> and you dont really have the choice - every society you could choose to be in, with the exception of yourself being a dictator, will have such people

in ancient times, you could banish people from the village

> engineers are expected to read the data sheet

even if you know what the data sheet says, it's easier said than done, especially when the tool gives you basically no help. you are just praying people will magically just git gud.

in my mind it would be doing what fil-c does for c to unsafe rust: a hypothetical memory safe implementation of unsafe rust using the same methods fil-c does e.g. gc

what would fil-rust do that miri doesn't?

> With non-deterministic tests I would always wonder if it's going to fail randomly after the code is already in production.

if you didn't use property-based testing, what are the odds you would've thought of the case?

it seems like the clean syntax makes the type checker's life harder and so performance is unacceptable. would you rather have clean syntax or acceptable compile times?

そんな暇ねぇよ

if it was in c, who knows how many memory corruption bugs would be found before they stumbled upon this...

they are memory safe

swift and rust?

in this example, aren't the scoping rules for c pretty much the same?

what do the annotations for the tool look like? is the analysis local, in that it doesn't look into the bodies of other functions? if it is, surely you would have to have lifetimes and be generic over them.

how much c code satisfies the tool? if there's hardly any c satisfying the tool, there might actually be a larger ecosystem of rust code to use.

> there are products that offer memory-safety proofs for C

what does the c checked by this tool look like? for an example like https://play.rust-lang.org/?version=stable&mode=debug&editio... , does the tool accept the assignment with f and reject the assignment with g?

stomping on in-bounds data might result in "nondeterminism", but bounded and not ub, which is unbounded.

because setting up and using anki is a pain? using and configuring anki is not intuitive. if you're just starting, you'll probably need to find a good premade vocab deck. once that's done, you'll need to make cards. making cards manually is a pita, i would probably not make any if i didn't have a good mining setup (yomitan/ttsu reader/asbplayer). i've spent countless hours getting my mining setup just right (setting up anki and yomitan, tweaking card fields/templates). yomitan probably works well because japanese conjugation is so regular. i imagine for languages with less regular conjugation, it wouldn't be so nice.

not if the app blocks screenshots

what happens when the legacy code is migrated to the new java, which is supposedly easier to upgrade post java 8? who will pay for long term support if upgrading is so easy?

wouldn't byte in rust be more like MaybeUninit<u8>, to account for uninit and pointer fragments?

the proof is so complicated it's hard to trust if it's only on paper. if we formalize it, it can be checked by a computer.

> Rust just survived by lying about the its safeties.

strong claim. care to back it up?