Rust-for-Linux VS dafny

You're welcome.

> Any concerns of the same kind of thing?

Here's the canonical list: https://github.com/Rust-for-Linux/linux/issues/2

There's a lot, and I don't know the status of many of them, personally. But I don't see anything there that I know is not gonna work out, like for example, they aren't using specialization. Most of it feels like very nuts and bolts codegen options and similar things.

That said, back in August, the Rust Project announced their goals for the second half of this year: https://blog.rust-lang.org/2024/08/12/Project-goals.html

They say that they're committed to getting this stuff done, and in particular: https://rust-lang.github.io/rust-project-goals/2024h2/rfl_st...

> Closing these issues gets us within striking distance of being able to build the RFL codebase on stable Rust.

So, things sound good, in my mind.

The goal of rust for linux isn't to wholesale translate linux into rust, but simply to be able to write pieces of linux (largely new ones) in rust. I think it's very unlikely anyone (including google) will take on a wholesale translation anytime soon. That said

> It's unlikely that Google has much sway here

Google has helped fund the rust for linux project pretty much from the start [1], they're one of three organizations mentioned on the homepage due to their sponorship [2]. They're actively involved in it, and have already ported their android "binder" driver into it with the intent to ship it in android. This strikes me as a very weird take.

[1] https://www.memorysafety.org/blog/supporting-miguel-ojeda-ru...

[2] https://rust-for-linux.com/

Rust is backwards compatible when you stick to stable features, but the kernel uses unstable features that can and do incur breaking changes.

https://github.com/Rust-for-Linux/linux/issues/2

> How would this work?

Don't know exactly what you're asking.

> And why would it be a better idea?

Poorly written device drivers are a significant attack vector. It's one of the reasons Linux is now exploring using Rust for its own device drivers.[0] You may be asking -- why Rust and not some other language? Rust has many of the performance and interoperability advantages of C and C++, but as noted, makes certain classes of memory safety issues impossible. Rust also has significant mindshare among systems programming communities.

[0]: https://rust-for-linux.com

Rust-for-Linux issue tracker

Automation of Hoare logic is quite good these days. Dafny, from MS Research (https://dafny.org), is probably the most friendly formal language. Dafny has been used to verify large systems, including many components of AWS. I am hoping that LLMs make more advanced languages, such as Liquid Haskell or Agda, much easier to write. Ideally, lots of code should be autocompleted once a human provides a type signature. The advantage of formal verification is that we are sure the generated code is correct.

Modern software verification employs various approaches, each offering different trade-offs between ease of use and strength of guarantees. AWS contributes to the open source program verification tools used in the previous examples. Dafny and Kani represent two powerful approaches to program verification. Let's see how they work in practice before connecting the dots between automated reasoning and generative AI.

On that note, I discovered Dafny[1] recently, as a more accessible way to program with proofs. There's a companion book[2] that seems very accessible and down-to-earth (and, unfortunately, quite expensive). I didn't have the time to play with it yet, but it looks like it does what Ada/SPARK does (and more), but with less verbose syntax and more options for compilation targets. It seems to be actively developed, too. Personally, I had a very hard time getting into Coq, which is a proof assistant more than a programming environment - Dafny seems much more welcoming for a "working programmer" :)

[1] https://dafny.org/

[2] https://mitpress.mit.edu/9780262546232/program-proofs

https://dafny.org/ also allows proof checking and allows do write real programs with it. It has a java like syntax and is also from MS I believe

> I do think there's a bit of the Ignaz Semmelweis[1] issue at hand here, where developers want to believe in their inherent quality and refuse processes that improve safety if it goes against their worldview

I think the problem is that other variables (not only safety) must be assessed beyond the pure "better". Haskell is very good also. Very correct. Who uses that, and where? And why? Why not everyone uses https://dafny.org/ ?

For those that are interested but perhaps not aware in this similar project, Dafny is a "verification-aware programming language" that can compile to rust: https://github.com/dafny-lang/dafny

Code correctness is a lost art. I requirement to think in abstractions is what scares a lot of devs to avoid it. The higher abstraction language (formal specs) focus on a dedicated language to describe code, whereas lower abstractions (code contracts) basically replace validation logic with a better model.

C# once had Code Contracts[1]; a simple yet powerful way to make formal specifications. The contracts was checked at compile time using the Z3 SMT solver[2]. It was unfortunately deprecated after a few years[3] and once removed from the .NET Runtime it was declared dead.

The closest thing C# now have is probably Dafny[4] while the C# dev guys still try to figure out how to implement it directly in the language[5].

[1] https://www.microsoft.com/en-us/research/project/code-contra...

[2] https://github.com/Z3Prover/z3

[3] https://github.com/microsoft/CodeContracts

[4] https://github.com/dafny-lang/dafny

[5] https://github.com/dotnet/csharplang/issues/105