I'm pleased to read Signal looks good to our robot mindlords.
p-e-w•10m ago
It’s nothing short of amazing that a huge codebase like Signal’s is apparently not only secure in a practical sense, but secure even in a strict formal sense. The people who wrote the Signal code must be engineers of the highest caliber.
Aboutplants•5m ago
Yeah quite impressive.
yread•9m ago
They thank Sundar Pichai. I guess it makes sense but at the same time...
paganel•8m ago
I'm not at all versed in this "formal proofing" thing, but without diving all that much into it how does this handle the halting problem (and the related problems that in the end all point to said halting problem)?
xrisk•5m ago
lean has no relation to the halting problem; you can think of it as a language that allows proofs to be encoded as code, and the compiler that runs that code as knowing how to enforce mathematical constraints appropriately
NooneAtAll5•4m ago
do you mean how is halting problem not a blocker or how halting problem itself is proven?
answer to the first is same as always - by simply not guaranteeing that everything is provable, especially in finite amount of time
xrisk•8m ago
wonder how many dollars were spent on this
nurumaik•5m ago
Now pls do telegram to settle "telegram shouldn't have invented their own crypto" debate once and for all
Computer0•15m ago