This is a n objectively false statement.

Rusts borrow checker is only able to prove at compile-time that a subset of correct programs are correct. There are many correct programs that the BC is unable to prove to be correct and therefore rejects them.

I’m a big fan of Rust and the BC. But let’s not twist reality here.

▲

lmm 5 hours ago | parent | next [-]

> There are many correct programs that the BC is unable to prove to be correct and therefore rejects them.

There are programs that "work" but the reason they "work" is complicated enough that the BC is unable to understand it. But such programs tend to be difficult for human readers to understand too, and usually unnecessarily so.

▲

ycombinatrix 2 hours ago | parent | prev [-]

>There are many correct programs that the BC is unable to prove to be correct and therefore rejects them.

No. The borrow checker rejects programs that are definitely incorrect. It does not require that the program is correct.

That's a big difference.

	▲	ChadNauseam 2 hours ago \| parent [-]
		there’s a miscommunication. programs that pass the borrow checker all are memory safe (assuming code marked unsafe is sound). This means that all memory unsafe programs are excluded. but some memory-safe programs are excluded too.