zz
unsafe-code-guidelines
zz | unsafe-code-guidelines | |
---|---|---|
10 | 74 | |
1,604 | 640 | |
- | 1.3% | |
1.9 | 6.9 | |
almost 2 years ago | about 2 months ago | |
Rust | ||
MIT License | Apache License 2.0 |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
zz
- A "logical" compiler
-
Is it possible to have a superset of the C programming languages standard that is as safe as Rust?
There is this: https://github.com/zetzit/zz
-
ISO C became unusable for operating systems development
You're right that you can't define a safe subset of C without making it practical. MISRA C defines a C subset intended to help avoid C's footguns, but it still isn't actually a safe language. There are alternative approaches though:
1. Compile a safe language to C (whether a new language or an existing one)
2. Formal analysis of C, or of some practical subset of C, to prove the absence of undefined behaviour
Work has been done on both approaches.
ZZ compiles to C. [0] Dafny can compile to C++, but it seems that's not its primary target. [1][2]
There are several projects on formal analysis of C. [3][4][5][6]
[0] https://github.com/zetzit/zz
[1] https://github.com/dafny-lang/dafny
[2] https://dafny-lang.github.io/dafny/
[3] https://frama-c.com/
[4] https://www.microsoft.com/en-us/research/project/vcc-a-verif...
[5] https://www.eschertech.com/products/ecv.php
[6] https://trust-in-soft.com/
-
Foundations of Dawn: The Untyped Concatenative Calculus
Formal methods have been used successfully for decades; it's not just a pipe dream. Perfect software should ideally be something like ultra-low-defect software, though (that's the term the AdaCore folks use).
There are also other projects that aim to make formal software development much easier [0][1] and of course there's SPARK Ada.
[0] https://github.com/zetzit/zz
[1] https://github.com/dafny-lang/dafny
- ZetZ: A zymbolic verifier and tranzpiler to bare metal C Resources
-
Programming in Z3 by learning to think like a compiler
This post reminds me that I've been wanting to try out ZetZ[0]. It incorporates Z3 into a high-level programming language, and seems to do a lot of what the post talks about automatically.
[0] https://github.com/zetzit/zz
-
Grids in Rust, part 2: const generics
I still want to try the ZZ language (https://github.com/zetzit/zz) someday. It compiles to C, and uses a SMT solver to prove that you don't index out-of-bounds at compile time. But I don't like how it lacks generics, uses C idioms, and compiles to C.
-
Another technique to manage memory
The zz language uses a SMT solver to check for program soundness... I haven't tried it, but that's got to be more flexible and resource-hungry.
-
We are building a new systems programming language
Especially the fact that it outputs C code. So interop is seamless.
https://github.com/zetzit/zz
For any systems language, interop with C is the litmus test.
With that in mind, this new language should not require 15,000 lines of standard library. A type-safe wrapper for libc should be enough...
-
Does such a language already exist ("Rust--")?
You might find ZetZ interesting!
unsafe-code-guidelines
-
Passing nothing is surprisingly difficult
Useful context on the Rust side is this issue [1]. It sounds like some of the author's concerns are addressed already.
[1]: https://github.com/rust-lang/unsafe-code-guidelines/issues/4...
-
Blog Post: Non-Send Futures When?
Is this captured by one of the known soundness conflicts? If not then should consider adding it to the list.
- Are crates like vcell and volatile cell still unsound?
-
Question: Are there things for Unsafe Rust learn from Zig?
There are some competing proposals for different memory models. Stacked borrows is the current proposal, but there are more work in the approproate WG.
-
Let's thank who have helped us in the Rust Community together!
Thank you /u/RalfJung for bringing formal methods to Rust, both through models like Stacked Borrows, by developing miri, and by working on unsafe-code-guidelines which aims to specify exactly what is and isn't allowed in unsafe code (surprisingly, it's an open question as 2023!)
- Questions about ownership rule
-
Noob Here: Why doesn't this work?
You could imagine some way to make this safe for example automatically convert &'short &'long mut T to &'short &'short T, but it's non-trivial to prove they are safe at all, not to mention ensuring this is correctly implemented in the compiler. If you're interested there's also a discussion on whether the opposite (& & T to & &mut T) is sound here.
-
When Zig is safer and faster than (unsafe) Rust
Agreed! MIRI is so good, it still feels like magic to me. It also comforts me that the Rust team takes improving unsafe semantics seriously, with the past Unsafe Code Guidelines WG and today's operational semantics team (t-opsem).
-
Safety and Soundness in Rust
I think there are some aspects of this rule that are still undecided. See for example:
- https://github.com/rust-lang/unsafe-code-guidelines/issues/8...
- https://github.com/rust-lang/miri/issues/2732
-
I wanna be a crab.
C is much better specified than unsafe Rust. Some things are just not worked out yet in Rust. This may sometimes even bite very experienced devs, such as this issue with Box's aliasing semantics, which tripped up the author of left-right.
What are some alternatives?
TinyGo - Go compiler for small places. Microcontrollers, WebAssembly (WASM/WASI), and command-line tools. Based on LLVM.
tokio - A runtime for writing reliable asynchronous applications with Rust. Provides I/O, networking, scheduling, timers, ...
checkedc - Checked C is an extension to C that lets programmers write C code that is guaranteed by the compiler to be type-safe. The goal is to let people easily make their existing C code type-safe and eliminate entire classes of errors. Checked C does not address use-after-free errors. This repo has a wiki for Checked C, sample code, the specification, and test code.
rust - Empowering everyone to build reliable and efficient software.
angr - A powerful and user-friendly binary analysis platform!
rfcs - RFCs for changes to Rust
CrossHair - An analysis tool for Python that blurs the line between testing and type systems.
x11rb - X11 bindings for the rust programming language, similar to xcb being the X11 C bindings
micro-mitten - You might not need your garbage collector
bevy - A refreshingly simple data-driven game engine built in Rust
alive2 - Automatic verification of LLVM optimizations
miri - An interpreter for Rust's mid-level intermediate representation