Help Define Rust Working and How Proof it?

Hello I am newbie and noob in Rust, my basic Haskell. My Friends suggest to try Rust similiar style with Haskell.

After 3 month learn Rust, i feel bit confused with Rust compare Haskell

Rust have define immutable similiar Haskell, and it work varibel not mutable.

Yeah its WORK have power IMMUTABLE = TRUE but ..

  1. How to PROOF that work called immutable mut ?
    Check output Assembly or Debug something compare same with Haskell work ?

My assumsion safe from FP is limitation pointers work Haskell, Erlang, but RUST open pointers do what ever going to do.

Some people Rust define Function Programming Style with Nanny compiler, make more confuse.
Or Just Coding and Nanny will check.

  1. How figure out Rust work and proof that ?
    Check output Assembly or Debug something compare same with Haskell work ?

Update 6 Dec | Thanks @2e71828 and @ZiCog very helpfull to understand

Rust was originally developed without formal proofs, but some work has been completed in terms of proving its models correct.

Understanding and Evolving the Rust Programming Language - Ralf Jung

What's your native tongue ? Maybe we can find someone here (or in the community) who'll be able to talk with you directly

I am Malaysian, sorry for my grammer or english not good for you all of guys.

Edit : Nanny State Not Nanny Compiler :slight_smile:

Do you mind typing on your native language? So that perhaps other people that understand can read it directly

I do speak Indonesian, so I guess I can sort of try?


I wonder what level of proof you are asking for?

  1. 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.

  1. 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.

  1. 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.

1 Like

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'.

  1. Formal Proof


I love Rust because had Ownership different other lang and similiar power for FP, but i need proof it real value or just ...

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.


Aku jawab sejauh pengetahuan aku:

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

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.