I don’t think you’re wrong, but in 2019, I think that there might better uses of people’s time than proving memory safety _in addition_ to, for instance, the absence of side-channel and timing attacks.
-
-
-
No-one should write in C unless they have to! But we shouldn't be fatalistic and assume that writing in C has to be doomed either. Most Kernel, Network, Cryptography and Systems code is still in C for the foreseeable future - but even there, it can be wrangled!
- 3 more replies
New conversation -
-
-
Those are fair points and observations and what papers I’ve read seem to indicate. I think if I were to restate my position, I’d say that if you’re starting from a point in which formal verification is an important bar to meet, you could default to a memory safe language...
-
...and drop down to C/assembly when you need to. I would say *ring* is a good example of this, but my understanding is that the project’s history is exactly backwards from what I described.
- 1 more reply
New conversation -
-
-
You can do a lot in ATS :)
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
I mean, I’ll defer to you, but my impression is that even with dynamic checks, the overall effort required to prove correctness is significantly less than doing the equivalent in C.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Thanks for the background on *ring*! I didn’t know most of this, except for the Mozilla::pkix and the BoringSSL history. The divergence is really fascinating, and I’d love to learn more, but I think I should get out of Colm’s mentions
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.