> effect system (formerly keyword generics)

Any recent link about that? Specially one that calls it effect system rather than the old name keyword generics

Via an unreliable, linker-based hack.

#[no_panic] has false-positives, but no false-negatives. If it’s present, the code won’t panic and can’t panic.

Index access violation that “never happens” is the root of every buffer overflow, so I’m absolutely OK with the minimal overhead behind the bounds check for actual safety

I'll cop to the word "viable" doing a lot of heavy lifting there, but I have not yet seen a dependent typing system that is adequate for engineering work. There are research systems, yes, and there are many people doing laudable work on it, but when people on HN pine for "dependent type systems", I think they're talking about wanting to live in a world where most people who are programming today are instead programming in dependently-typed systems happily and productively, not a world where all programmers not functioning at a PhD-candidate level are evicted from the profession because they can't handle proof languages.

Or, to put it another way, there is no dependently-typed language I can even consider saying to my manager "Hey, you asked me to do X and I think I'll use language Y which is dependently typed", and as far as I can see, the problem isn't just that "nobody has built the standard library for it yet" or any thing else, the problem boils down to, they just aren't easy enough to use to call them practical.

I'd also say that "hey, you can use this dependently-typed language, just don't try to actually use the dependently-typed features" is also not what people are pining for.

> Dependent types are "only pay for what you prove" --- if you don't try to prove anything there is no problem.

I have to disagree with this, since fully general dependent types seem to inherently involve a kind of compile-time evaluation. You can recover a sort of phase distinction (i.e. a post-compile "run time" phase) but only AIUI through an "extraction" step that dispenses with the actual dependently typed parts of the program.

Buffer overflow vulnerabilities are prevented with bounds checking, but that just means you get a panic at runtime. With formal verification, you can prove that the program never accesses an array with an index that's out of bounds.

I guess you're asking why that wasn't built into Rust from the start; after all, there are programming languages with the formal verification and theorem-proving built-in, e.g. for imperative languages, the SPARK extension to Ada, as well as ATS, or for a functional one, Idris. My guess is that Rust never would have become popular if you needed to write actual formal proofs to guarantee some degree of safety, since satisfying the borrow checker is easier in comparison, and it also probably would have been a lot harder to develop Rust after that. The borrow checker simply eliminating use-after-free errors and data races in safe code was good enough.

Yes, it should make sure that there are not buffer overflows, but this is the next step.

Test verify that the code works on specific inputs. Formal verification checks that it works on every input.

But why? Tests can't catch everything. A single verified predicate is equivalent to a very large, potentially infinite number of tests.

Right now the Rust stdlib is being verified using Kani, a model checker, https://model-checking.github.io/verify-rust-std/

In Kani, a proof looks like this

https://github.com/model-checking/verify-rust-std/blob/00169...

    #[kani::proof_for_contract(NonNull::new_unchecked)]
    pub fn non_null_check_new_unchecked() {
        let raw_ptr = kani::any::<usize>() as *mut i32;
        unsafe {
            let _ = NonNull::new_unchecked(raw_ptr);
        }
    }

It looks like a test, but actually it is testing that every possible usize, when converted to a pointer to i32 and built with NonNull::new_unchecked, will follow the contract of NonNull::new_unchecked, which is defined here

https://github.com/model-checking/verify-rust-std/blob/00169...

    #[requires(!ptr.is_null())]
    #[ensures(|result| result.as_ptr() == ptr)]

Which means: if the caller guarantees that the parameter ptr is not null, then result.as_ptr() is the same as the passed ptr

That's a kind of trivial contract but Kani tests for all possible pointers (rather than some cherry picked pointers like the null pointer and something else), without actually brute-forcing them but instead recognizing when many inputs test the same thing (while still catching a bug if the code changes to handle some input differently). And this approach scales for non-trivial properties too, a lot of things in the stdlib have non-trivial invariants.

You can check out other proofs here https://github.com/search?q=repo%3Amodel-checking%2Fverify-r...

It's not that different from writing a regular test, it's just more powerful. And you can even use this #[requires] and #[ensures] syntax to test properties in regular tests if you use the https://crates.io/crates/contracts crate.

Really if you have ever used the https://proptest-rs.github.io/proptest/intro.html or the https://crates.io/crates/quickcheck crate, software verification is like writing a property test, but rather than testing N examples generated at random, it tests all possible examples at once. And it works when the space of possible examples is infinite or prohibitively large, too.

Say I have as input a byte. I create a test that exercises every possible byte value.

A verification would be the equivalent of that. In practice that matters since the input space is often much larger than just one byte.