I'm more optimistic. There's real value in building ultra-low-defect crypto code, and as far as I can tell, formal methods have a good track-record there. We al

I'm more optimistic. There's real value in building ultra-low-defect crypto code, and as far as I can tell, formal methods have a good track-record there. We already knew that integration into non-verified code isn't guaranteed to be free of defects - that's out of scope by definition. That's somewhere safe languages can help though. What the paper describes as corrupted data might well be the kind of bug that often happens in C, but rarely happens in a safe language. The other question is vulnerability to side-channel attacks. Today's formal methods aren't much use against them.