Compiling C to Safe Rust, Formalized

Would you mind expanding on this?

It sounds interesting, but I'm not tuned into either community enough to know what parallels you see.

With rust having recently entered the Linux kernel, Windows 11, qemu among others where Haskell never took a hold, I really fail to see where you feel the wind is blowing.

The thing is, rust is used today in more and more places because it's reliable. We're not going to switch out the ground we are standing on every time something shiny comes along and that's why this is such an interesting development.

What steps are you talking about? lambda calculus is one particular way to formalize program semantics, which is appropriate when talking about... program formalization

Even steel plated armour succumbs to rust given the environment and time

Just because you have tiny pieces being written in it doesnt mean its getting adopted. Its way too cumbersome to write entire OS in it - all the example projects like AWS Firecracker end up with tons of unsafes. And its runtime components for dynamic memory stuff eat into efficiency.

Basically a more expansive and possibly ML powered valgrind can easily offer the same memory safety as Rust does, without the penalty of slower development and efficiency hits, so Rust adoption is "unstable" i.e its just a nice improvement but not does not give a hard advantage in any form and way.

Lambda calculus is a thing that stays in colleges. Nobody uses it in the real world. Computers are imperative by design. Any community that tries to to apply some abstract theory to tools used in the real world is doomed to fail from the start.

Haskell philosophy is basically asumming that programmers were really bad at parallelism and thread saftey, and thus it was made to address this concern. However because that overarching idea is ideological in nature (i.e not true as a statement about programmers as a whole), the community was prevalent with ideology, using a lot of lambda calculus notation to set itself apart, and making coding in it cumbersome. As a result, nobody bothered to really do anything with it.

Rust has largely the same problem. You see bits of use of it here and there, but its also based in ideology that programmers are bad at managing memory.

From a technical viewpoint, Rust doesnt offer anything that doesnt already exist, while providing a more cumbersome way to code. Which is why its a days are numbered.

I clearly remeber seeing replies similar to yours from the Haskell fans:)

Haskell was most certainly not made to address a concern about programmers being really bad at parallelism and thread safety.

It absolutely has. The functional programming paradigm is designed specifically to describe a program withoilut side effects, so you can be sure that execution is deterministic (and thus scalable and parallelizable). There are no other advantages to functional programming.

> Its way too cumbersome to write entire OS in it

Not at all. See https://www.redox-os.org/

and many more: https://github.com/flosse/rust-os-comparison

> all the example projects like AWS Firecracker end up with tons of unsafes.

That's a good thing. With rust you are explicit about unsafe.

> Basically a more expansive and possibly ML powered valgrind can easily offer the same memory safety as Rust does, without the penalty of slower development and efficiency hits

It is apparent that you have no experience from rust, and I wonder if you have used valgrind much too, as you seem unaware about the huge overhead from running your app through valgrind.

Rust's error messages are precise, while valgrind is a crapshow to work with, as you should know since you mentioned it?

> so Rust adoption is "unstable" i.e its just a nice improvement but not does not give a hard advantage in any form and way.

It's used in production in several high profile projects, some that I already mentioned. Apparently smart people do see advantages.