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.

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.