Ask HN: Why isn't Proof-Carrying Code more popular?

It seems that Typed Assembly Language and the notion of Proof-Carrying Code have proved that you can ship binaries that contain formal guarantees of certain properties, like memory-safety.

This approach seems like it completely abstracts away all the arguments about which language offers the best guarantees, and moves the checks to installation-time instead of compile-time.

This is important because a shipped binary needs to be trusted, and if you think the binary is written in safe Rust or whatever, then that may give you peace of mind. But you have no guarantee what the binary actually is, and a single instance of memory-unsafety could be a backdoor. You have to just take a leap of faith with the entire supply chain.

It is as if we, as a society, have chosen to rely entirely on client-side validation without ever actually validating server-side.

PCC and TAL could obviate the entire issue, without new exotic hardware like CHERI.