3 ms·

I checked them, but I am not convinced and I am not sure why it was brought into this thread. SPARK has industrial-strength, integrated verification proven in

• afdbcreid 1y ago
  I think I did say: > although none is as integrated as SPARK I believe And yes, they're experimental (for now). But some are also used in production. For example, AWS uses Kani for some of their code, and recently launched a program to formally verify the Rust standard library. Whether the language was designed for it does not matter, as long as it works. And it works well. > `unsafe` blocks create unverifiable boundaries Few of the tools can verify unsafe code is free of UB, e.g. https://github.com/verus-lang/verus https://github.com/verus-lang/verus. Also, since unsafe code should be small and well-encapsulated, this is less of a problem. > the trait system and lifetime inference are too complex to model completely You don't need to prove anything about them: they're purely a type level thing. At the level these tools are operating, (almost) nothing remains from them. > procedural macros generate code that can't be statically verified The code that procedural macros generate is visible to these tools and they can verify it well. > interior mutability (`Cell`, `RefCell`) bypasses type system guarantees Although it's indeed harder, some of the tools do support interior mutability (with extra annotations I believe). > Rust can panic in safe code That is not a problem - in fact most of them prove precisely that: that code does not panic. > Most critically, Rust lacks a formal language specification with mathematical semantics That is a bit of a problem, but not much since you can follow what rustc does (and in fact it's easier for these tools, since they integrate with rustc). > Rust's semantics are informally specified and constantly evolving (async, const generics, GATs) Many of those advancements are completely erased at the levels these tools are operating. The rest does need to be handled, and the interface to rustc is unstable. But you can always pin your Rust version. > This isn't tooling immaturity though, it's a consequence of language design. No it's not, Rust is very well amenable to formal verification, despite, as you said, not being designed for it (due to the shared xor mutable rule, as I said), Perhaps even more amenable than Ada. Also this whole comment seems unfair to Rust since, if I understand correctly, SPARK also does not support major parts of Ada (maybe there aren't unsupported features, but you not all features are fully supported). As I said I know nothing about Ada or SPARK, but if we compare the percentage of the language the tools are supporting, I won't be surprised if that of the Rust tools is bigger (despite Rust being a bigger language). These tools just support Rust really well.
  • johnisgood 1y ago
    > Whether the language was designed for it does not matter, as long as it works. And it works well. It matters fundamentally. "Works well" for research projects or limited AWS components is not equivalent to DO-178C Level A certification where mathematical proof is required. The verification community distinguishes between "we verified some properties of some code" and "the language guarantees these properties for all conforming code." > Few of the tools can verify unsafe code is free of UB With heavy annotation burden, for specific patterns. SPARK has no unsafe - the entire language is verifiable. That's the difference between "can be verified with effort" and "is verified by construction." > You don't need to prove anything about [traits/lifetimes]: they're purely a type level thing Trait resolution determines which code executes (monomorphization). Lifetimes affect drop order and program semantics. These aren't erased - they're compiled into the code being verified. SPARK's type system is verifiable; Rust's requires the verifier to trust the compiler's type checker. > The code that procedural macros generate is visible to these tools The macro logic is unverified Rust code executing at compile time. A bug in the macro generates incorrect code that may pass verification. SPARK has no equivalent escape hatch. > some of the tools do support interior mutability (with extra annotations I believe) Exactly - manual annotation burden. SPARK's verification is automatic for all conforming code. The percentage of manual proof effort is a critical metric in formal verification. > That is not a problem - in fact most of them prove precisely that: that code does not panic So they're doing what SPARK does automatically - proving absence of runtime errors. But SPARK guarantees this for the language; Rust tools must verify it per codebase. > you can follow what rustc does (and in fact it's easier for these tools, since they integrate with rustc) "Follow the compiler's behavior" is not formal semantics. Formal verification requires mathematical definitions independent of implementation. This is why SPARK has an ISO standard with formal semantics, not "watch what GNAT does." > Rust is very well amenable to formal verification [...] Perhaps even more amenable than Ada Then why doesn't it have DO-178C, EN 50128, or ISO 26262 certification toolchains after a decade? SPARK achieved this because verification was the design goal. Rust's design goals were different - and valid - but they weren't formal verifiability. > SPARK also does not support major parts of Ada Correct - by design. SPARK excludes features incompatible with efficient verification (unrestricted pointers, exceptions in contracts, controlled types). This is intentional subsetting for verification. Claiming Rust tools "support more of Rust" ignores that some Rust features are fundamentally unverifiable without massive annotation burden. The core issue: you're comparing research tools that can verify some properties of some Rust programs with significant manual effort, to a language designed so that conforming programs are automatically verifiable with mathematical guarantees. These are different categories of assurance.
• debugnik 1y ago
  > SPARK has no escape hatches It does, you can declare a procedure in SPARK but implement it in regular Ada. Ada is SPARK's escape hatch. This is just as visible in source code as unsafe is in Rust, a procedure body will have SPARK_Mode => Off.
  • johnisgood 1y ago
    Yes, SPARK provides an explicit escape hatch, but it is meaningfully different from Rust's `unsafe`. In SPARK: you keep the spec in the verifiable world (a SPARK-visible subprogram declaration) and place the implementation outside the proof boundary (for example in a body or unit compiled with `pragma SPARK_Mode(Off)`). The body is visible in source but intentionally opaque to the prover; callers are still proved against the spec and must rely on that contract. In Rust: `unsafe` is a lexical, language-level scope or function attribute that disables certain compiler/borrow checks for the code inside the block or function. The unchecked code remains inline and visible; the language/borrow-checker no longer enforces some invariants there, so responsibility shifts to the programmer at the lexical site. Practical differences reviewers should understand: - Granularity: `unsafe` is lexical (blocks/functions); SPARK's hatch is modular/procedural (spec vs body). - Visibility: Rust's unchecked code is written inline and annotated with `unsafe`; SPARK's unchecked implementation is placed outside the prover but the spec remains visible and provable. - Enforcement model: Rust's safety holes are enforced/annotated by the compiler's type/borrow rules (caller and callee responsibilities are explicit at the site). SPARK enforces sound proofs on the interface; the off-proof body must be shown (by review/tests/docs) to meet the proven contract. - Best practice: keep off-proof bodies tiny, give strong pre/postconditions on the SPARK spec, minimize the exposed surface, and rigorously review and test the non-SPARK implementation. TL;DR: `unsafe` = "this code block bypasses language checks"; SPARK's escape hatch = "this implementation is deliberately outside the prover, but the interface is still what we formally prove against."
    • aw1621107 1y ago
      I'm not sure I see much of a difference still. Here's what I think is a more correct Rust comparison: > In [Rust]: you keep the spec in the verifiable world (a [type checker-visible function signature]) and place the implementation outside the proof boundary (for example in a body or unit compiled with `unsafe`). The body is visible in source but intentionally opaque to the [type checker; callers are still proved against the spec and must rely on that contract. These "practical differences" seem questionable to me as well. > Granularity: `unsafe` is lexical (blocks/functions); SPARK's hatch is modular/procedural (spec vs body). `unsafe` can trivially be expanded from a block to a function body, thereby transforming it to a "modular/procedural" hatch. `unsafe` on function signatures is more akin to SPARK's `Assume`, albeit with the precise assumption (hopefully) in the documentation. > Visibility: Rust's unchecked code is written inline and annotated with `unsafe` This... doesn't seem like a difference to me? According to you, you can place SPARK's unchecked code "in a body [] compiled with `pragma SPARK_Mode(Off)`". That sure sounds like writing unchecked code "inline" and annotated with SPARK's equivalent of `unsafe` to me. > SPARK's unchecked implementation is placed outside the prover but the spec remains visible and provable. You can say an analogous thing about Rust: The unchecked implementation is placed outside the [type checker] but the [function signature] remains visible and [checkable]. > Enforcement model: Rust's safety holes are enforced/annotated by the compiler's type/borrow rules (caller and callee responsibilities are explicit at the site). This is... confusing? I'm honestly not sure what you're trying to get at. > SPARK enforces sound proofs on the interface; the off-proof body must be shown (by review/tests/docs) to meet the proven contract. The Rust equivalent is a non-`unsafe` function signature with an `unsafe` body, and what you say is equally as applicable. > Best practice: keep off-proof bodies tiny, give strong pre/postconditions on the SPARK spec, minimize the exposed surface, and rigorously review and test the non-SPARK implementation. This... doesn't describe a difference at all? It's equally as applicable to the analogous Rust construct. > `unsafe` = "this code block bypasses language checks" Technically wrong? Bit of a nitpick, but `unsafe` technically does not disable any language checks; it gives you access to unchecked capabilities. It's a slight difference but an important one, since it means that if you have code that doesn't compile and doesn't use unchecked capabilities (e.g., a borrow checking error with regular references), wrapping the code in `unsafe` will not allow your code to compile. > SPARK's escape hatch = "this implementation is deliberately outside the prover, but the interface is still what we formally prove against." Again, you can say basically the same thing for non-`unsafe` functions in Rust.