←back to thread

278 points love2read | 3 comments | | HN request time: 0.618s | source
Show context
wffurr ◴[] 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 #
1. medo-bear ◴[] No.42479358[source]
What is the benefit of compiling formally correct code to Rust? It seems that all the possible benefits are already there (if not more)
replies(1): >>42480064 #
2. gpm ◴[] No.42480064[source]
I suppose hypothetically putting it in an easier language to make changes in. Though it's hard to imagine it being easier to make changes to transpiled code than the original.

Alternatively this might be seen as a stepping stone to translating non-formally-verified C to rust, which I understand the US government has expressed a fair bit of interest in.

replies(1): >>42480100 #
3. medo-bear ◴[] No.42480100[source]
Good luck with both of that. Otherwise people whose dayjob is rewritting everything in Rust will soon be out of a job