Almost every "safe" language is itself written in C though. That's the key; use C very minimally for the bottom layer, and then build on top of abstractions. Or write C like LISP; build an inner safe DSL, and then use that. That's been our approach.https://twitter.com/glyph/status/1120524418906824705 …
-
-
Replying to @colmmacc
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.
1 reply 0 retweets 0 likes -
Replying to @BRIAN_____ @colmmacc
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.
0 replies 0 retweets 0 likes -
Replying to @BRIAN_____ @colmmacc
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...
1 reply 0 retweets 0 likes -
...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 reply 0 retweets 0 likes
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.