4 ms·
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 sti
by xvedejas 1y ago
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 1y agoIt 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 1y agohttps://github.com/CertiCoq/certicoq https://github.com/CertiCoq/certicoq can prove (most of) itself.
- burnt-resistor 1y agoThe 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.