Make formal verification and provably correct software practical and mainstream

Post by blainehansen » Sat, Jun 04, 2022, 4:53 AM UTC

AnimalMuppet wrote: post #52

hn_urbit_thr123 wrote: post #43

Is it even realistic to make a provably secure/stable applications on an OS like windows or linux? This (provable correctness of programs, at the expense of performance) is one of the explicit design goals or urbit. I know HN hates urbit and don't want to rehash that, but it seems like a good goal for some use cases and I'm not sure it's possible to achieve without building the OS around it.

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 essenti…

Post by blainehansen » Sat, Jun 04, 2022, 4:56 AM UTC

xavxav wrote: post #79

Honestly, to me this project is a means seeking an end, the same way JS devs love to play around with frontend frameworks, the author saw a bunch of shiny powerful (highly complex) tools and decided that combining them all was the solution to our problems. I don't want to discourage them from learning Iris, or designing a dependently typed language, but I really think that's missing the difficulty in formal verificat…