Most active commenters
  • medo-bear(10)
  • keybored(6)
  • woodruffw(3)

←back to thread

Compiling C to Safe Rust, Formalized

(arxiv.org)
291 points love2read | 19 comments | 20 Dec 24 23:30 UTC | HN request time: 0.829s | source | bottom
Show context
wffurr ◴[21 Dec 24 00:33 UTC] No.42476523[source]▶
Note that this is done for “existing formally verified C codebases” which is a lot different from typical systems C code which is not formally verified.
replies(8): >>42476623 #>>42477360 #>>42478051 #>>42478440 #>>42478560 #>>42478707 #>>42479358 #>>42479797 #
akkad33 ◴[21 Dec 24 10:09 UTC] No.42478707[source]▶
Is Rust formally verified? Not that I know of
replies(3): >>42478873 #>>42480047 #>>42480818 #
PartiallyTyped ◴[21 Dec 24 10:46 UTC] No.42478873[source]▶
You can always run model checkers like Kani, though even that is limited.
replies(1): >>42479351 #
medo-bear ◴[21 Dec 24 12:43 UTC] No.42479351[source]▶
So no?
replies(1): >>42479779 #
johnisgood ◴[21 Dec 24 14:10 UTC] No.42479779[source]▶
The answer is that it is not.

It frustrates me more than it should, I admit, that people always mention Rust when they talk about safety, but never Ada / SPARK. You want formal verification? Use Ada / SPARK. It has been battle-tested. It has been used for critical systems for a really long time now.

(And a compiler being formally verified vs. being able to write formally verified code means two different things.)

replies(3): >>42479874 #>>42484006 #>>42489910 #
medo-bear ◴[21 Dec 24 14:26 UTC] No.42479874[source]▶
I think a disclaimer like this should be written with every Rust application, like health warnings on cigarette packets
replies(1): >>42479893 #
johnisgood ◴[21 Dec 24 14:30 UTC] No.42479893[source]▶
At this point, I think that would be better, yes, just because people think Rust is "fully" safe, which is just incorrect. I think the problem was the Rust hype and repeated statements of it being very safe, so we have some undoing to do.

For example if someone on GitHub sees that the project is written in Rust, they are automatically going to assume it is safe, incorrectly so. I do not blame them though.

replies(2): >>42480248 #>>42480314 #
1. keybored ◴[21 Dec 24 15:39 UTC] No.42480248[source]▶
You presumably extend this to every virtual machine or interpreter for every language which is implemented in an unsafe language. When that language claims to be safe (like all such languages claim to be).

That seems excessive and tedious.

replies(1): >>42480329 #
2. medo-bear ◴[21 Dec 24 15:52 UTC] No.42480329[source]▶
The point, I think, was that "safety" presumptions about Rust are often exaggerated or poorly misunderstood due to hype. That could certainly lead to problems
replies(2): >>42480572 #>>42481051 #
3. woodruffw ◴[21 Dec 24 16:36 UTC] No.42480572[source]▶
I don’t think Rust’s actual safety properties aren’t overhyped, although they may be subject to misunderstanding about their exact extent.

Concretely: spatial and temporal memory safety are good things, and Rust achieves both. It’s not unique in this regard, nor is it unique in not having a formal definition.

replies(2): >>42484831 #>>42485908 #
4. keybored ◴[21 Dec 24 17:49 UTC] No.42481051[source]▶
> The point, I think, was that "safety" presumptions about Rust are often exaggerated or poorly misunderstood due to hype. That could certainly lead to problems

Then the point is hypocritical.

Runtimes for safe programming languages have been implemented in unsafe languages since the dawn of safe programming languages, basically.

EDIT: I see now that you are the cigarette warning guy. In that case I don’t understand what this coy “I think” speculation is about when you made such a bizarre proclamation on this topic.

replies(1): >>42482241 #
5. medo-bear ◴[21 Dec 24 20:58 UTC] No.42482241{3}[source]▶
Your tendency to answer jokes so seriously is a symptom of the hype
replies(2): >>42482642 #>>42483003 #
6. keybored ◴[21 Dec 24 21:55 UTC] No.42482642{4}[source]▶
Me being humorless (read: not just rolling with your cop-out) is a symptom of the Rust hype.

Doesn’t even make sense.

replies(1): >>42483244 #
7. jeltz ◴[21 Dec 24 22:56 UTC] No.42483003{4}[source]▶
Your irrational hate for a programming language adds nothing to the discussion.
replies(1): >>42483255 #
8. medo-bear ◴[21 Dec 24 23:42 UTC] No.42483244{5}[source]▶
you feeling the need to defend it at every jibe. chill. rust is not a cult
replies(2): >>42484828 #>>42484832 #
9. medo-bear ◴[21 Dec 24 23:43 UTC] No.42483255{5}[source]▶
so many powerful words lol
10. keybored ◴[22 Dec 24 07:02 UTC] No.42484828{6}[source]▶
A jibe is some sort of playful banter based on a literal or exaggerated truth. Since your comment does not lampoon any real deficiency except when being hypocritical, there is nothing to defend.

Maybe you should wear a sign on your torso: will make irrational points and then complain about persecution when that is pointed out. I don’t know. It’s just one more idea for when we decide to put all the anti-Rust people in camps.

replies(1): >>42485914 #
11. keybored ◴[22 Dec 24 07:04 UTC] No.42484831{3}[source]▶
Double negation makes things ambigious.
replies(1): >>42485249 #
12. mardifoufs ◴[22 Dec 24 07:04 UTC] No.42484832{6}[source]▶
It's weird to imagine for cniles but discussing a language doesn't inherently involve defending it, especially when it's just someone correcting someone else. I know, that's a very weird concept :^)
replies(1): >>42489095 #
13. woodruffw ◴[22 Dec 24 09:10 UTC] No.42485249{4}[source]▶
The second negation is a typo, but it’s too late to fix it.
14. medo-bear ◴[22 Dec 24 12:19 UTC] No.42485908{3}[source]▶
> although they may be subject to misunderstanding about their exact extent

Isnt that what overhype means? Also no one is saying that Rust is unique in being overhyped. It is true of almost any language worth writing in, including c, lisp, python, haskell, type script etc.

replies(1): >>42487300 #
15. medo-bear ◴[22 Dec 24 12:22 UTC] No.42485914{7}[source]▶
Its sunday, shouldnt you be in church of holy borrow checker?
replies(1): >>42485962 #
16. keybored ◴[22 Dec 24 12:37 UTC] No.42485962{8}[source]▶
Today is Java day.
17. woodruffw ◴[22 Dec 24 16:24 UTC] No.42487300{4}[source]▶
I don't see much overhype coming from Rust practitioners. I see a lot of people who care about spatial and temporal memory safety, for which the hype with Rust appears largely appropriate. I've yet to see people (incorrectly) extend this to a claim that Rust solves all security problems, which would meet the definition of overhype.

(If there's nothing unique here, it doesn't make sense to single any particular language out. But each language does have unique properties: Python is a great rapid development language, Rust offers zero-cost abstractions for memory safety, etc.)

replies(1): >>42488858 #
18. medo-bear ◴[22 Dec 24 20:32 UTC] No.42488858{5}[source]▶
> I don't see much overhype coming from Rust practitioners

That is like saying I don't see much overhype about AI from machine learning engineers. I am a ml engineer, and like myself great majority of ml engineers will tell you that there is certainly overhype about the field and do not engage in the overhype. Which is not to say that the field isnt producing some really cool results

> I've yet to see people (incorrectly) extend this to a claim that Rust solves all security problems, which would meet the definition of overhype.

Ive seen plenty of questionable Rust rewrites due to solving security problems

> Python is a great rapid development language

Saying to a Lisper that Python is a great rapid development language is like selling Rust safety to an Ada person :)

19. medo-bear ◴[22 Dec 24 21:05 UTC] No.42489095{7}[source]▶
Correcting what though ?