Proof that machine code generated by the compiler correctly implements what you have written in your source code given the semantics of the language.
Typically most people leave that to the compiler developers and trust they have done a good job. No matter what language. I have only ever worked on one project where a review of the generated assembler was required in case of compiler bugs. That was for a military secure communications project.
Some kind of proof that the source code you have written correctly implements whatever requirements you have. That is does what it should and does not do what it should not.
Typically most people do that by writing tests. Luckily Rust has good facilities for incorporating tests into ones projects. The sky is the limit when it comes to the level of testing you want to do. Usually impossible to cover every possible scenario the code will meet at run time.
Of course Rust helps with 2) with it's strict type checking and famously its checks for accidental misuse of memory, mutable, immutable access, multiple references etc at compile time. Again we generally trust the Rust language and compiler correctly checks these things.
Formal proofs that 2) is correct. As far as I know that is still impossible in the general case.
I'm not happy about the classification of languages into "Draconian", "free" or "nanny state". Seems to me there are languages that check ones use of memory and those that don't. Well, I only know one of the latter, Rust. This is incredibly valuable for helping to ensure correct code, especially in concurrent systems where memory misuse mistakes are easy to Mae in many languages and often very hard to debug.
saya bisa Bahasa Indonesia.
Basic Math and Haskell
Jadi saya ingin tahu, bagaimana Rust berkerja
Kita ambil example : keyword 'mut' nanti berkerja untuk immutable
Pada Rust dan Haskell, pakai variabel 'mut A' jadi tidak dapat berubah valuenya. Axiom = Asumi dapat berkarja makalah TRUE, tapi belum di Buktikan. Saya ingin tahu bagaimana membuktikan pada Rust, 'mut A' is TRUE immutable how proof it.
Setahu saya, FP layak Hasekelll berjalan di Pointers, tapi Rust berbeda saya ingin tahu rust berkerja.
It hard understand similiar Axioms in Math
example :
I have 1 egg, buy again 1 egg so i have 2 eggs now
similiar in math
1 + 1 = 2 = TRUE
but why 1 + 1 = 2 ?
it really real value 2, we need PROOF it
If we use Peano Axioms = a + 0 = a and bla... yeah its 2.
Apakah benar value 2, maka dibukti Pembukti.
similiar 'mut A' is TRUE immutable how proof it in Rust.
Reverse Engineering Rust or check assembly work like exe extractor or check machine memory or ooh.. it complier i dunno
Maybe similiar with 'Turning Incomplate' and 'Turning Complate'.
Rust was originally developed without formal proofs, but some work has been completed in terms of proving its models correct. See in particular the publications of the RustBelt project.
Buat point pertama, mut artinya mutable. Variable di Rust secara default itu immutable
Buat pembuktian secara "abtract mathematics"... sejauh ini aku tidak terlalu ngerti. Secara praktikal AFAIK tidak ada sesuatu yang "spesial" dari mutable/immutable di level assembly/machine code, mutable/immutable hanya berlaku pada high-level language, seperti Rust.
I'll try to answer as far as my understanding goes:
For the first point, mut means mutable. Variable is immutable by default on Rust
As for the proof of the mathematics... I don't really know much about that TBH. AFAIK there's nothing special about mutable/immutable on the low-level assembly code, it only applies to higher-level language like Rust
You might be interested in the RustBelt Project (oops didn't read @2e71828) if you're interested in a more "academic" background on Rust
