[AnimalMuppet]

Let's say that Urbit claims to be formally, provably secure. But approximately nobody actually understands Urbit, which means that nobody knows whether the proof is solid. So as an outsider, I have to either take it on faith that it's secure, or I have to spend a fair amount of time immersing myself in this hard-to-learn system to see if the claimed benefits are really there.

But it's not just Urbit. Rust has essentially the same problem.

In fact, perhaps all of formal verification has this kind of problem. How do you prove the benefits to someone who doesn't know the tools?

[blainehansen]

Hi, maintainer/author of Magmide here: https://github.com/magmide/magmide#is-it-actually-useful-to-...

[hn_urbit_thr123]

You don't have to understand the linux kernel to buffer overlow a linux application; If they do something like "Here's the IP of a running urbit with 100BTC in it, good luck!" and it's still up in a few years, that'd be compelling.

But more generally, if it's true that the only way to make a provably secure app is to design the OS and language around that purpose, then the problem you describe is general too - it will always be a challenge to find auditors.