[xvedejas]

Safe rust is a safe language. Yes, it is built upon unsafe rust. But I still consider Python to be a memory safe language despite it being built on C. I can still trust that my Python code doesn't contain such memory errors. Safe Rust is the same in terms of guarantees. That's all that anyone is claiming.

[UltraSane]

It is a lot like how you have to trust the core proving kernel in a theorem prover but if you do then you can trust every proof created using it.

[burnt-resistor]

https://github.com/CertiCoq/certicoq can prove (most of) itself.

[burnt-resistor]

The main problem now is that there isn't a platform that has the tooling or infrastructure to prove, including through formal methods, that they are correct and free from bugs in the spirit of the seL4 project.