[HN Gopher] Coq-of-rust: Formal verification tool for Rust
___________________________________________________________________
Coq-of-rust: Formal verification tool for Rust
Author : todsacerdoti
Score : 112 points
Date : 2025-03-14 08:34 UTC (3 days ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| jedisct1 wrote:
| Do that for Zig.
| arn3n wrote:
| Rust's "mutable-xor-aliased" model makes it particularly
| amenable to developing verification tools on top of it [1].
| Without this model, verification becomes just as hard -- and
| just as practically intractable -- as all the verifiers for
| existing languages.
|
| 1: https://graydon2.dreamwidth.org/312681.html
| johnisgood wrote:
| > Rust supports it better than many other imperative systems
| languages -- even some impure functional ones!
|
| I am surprised that this blog post does not mention Ada /
| SPARK at all though.
| gaugefield wrote:
| While this does not mention it, in many other discussions
| Rust vs Ada is mentioned. My (late) introduction to Ada via
| was finding out in one of the Rust forums.
| porridgeraisin wrote:
| The link returns 403.
| johnisgood wrote:
| It (still) works for me.
| SAI_Peregrinus wrote:
| > Even if Rust's type system prevents many mistakes, including
| memory errors, the code is still not immune to vulnerabilities,
| such as unexpected panics or wrongly implemented business rules.
|
| > The way to go further is to mathematically prove that it is
| bug-free: this is named "formal verification" and what coq-of-
| rust proposes! This is the only way to ensure your code contains
| no bugs or vulnerabilities, even against state-level actors .
|
| I _like_ formal verification. But I consider this a
| misrepresentation of what it offers. It lets you mathematically
| prove that your code implements a specification correctly. It
| doesn 't prove that your specification is bug-free &
| vulnerability-free. It doesn't prove that your specification
| correctly implements your business rules.
|
| Formal verification is still extremely useful. It's often much
| easier to use a specification language to define invariants your
| programming language code needs to obey than to only implement
| things in a programming language. To me _that 's_ a much better,
| more honest selling point for formal methods. You have to write
| more code, and in a different language, but unlike just testing
| you can actually prove that invariants hold for all possible
| inputs.
| amw-zero wrote:
| You are describing "validation": the process of verifying that
| your spec really says what you mean.
| nicce wrote:
| He is saying that original spec can be incorrect.
| jghn wrote:
| Yes. And the post you're replying to is pointing out that
| that would be part of `Validation` to decide. Verification
| is confirming the software meets the spec. Validation is
| confirming that the software meets the actual desired
| behavior.
| nicce wrote:
| I think the comment was way shorter than it currently is
| when I replied. It is sometimes difficult to say what is
| meant with "validation". Many also use it to mean
| "functional testing", for example, which is incorrect.
| jghn wrote:
| based on what amw-zero stated, they're using it in the
| formal QC sense like ISO9001. In that context the two
| words have distinct meanings.
|
| I do agree that colloquially they can be used in
| different ways, but as we're talking about formal
| verification as a concept, in this case verification
| aligns with that definition.
| Animats wrote:
| It's very useful for things where the specification is much
| simpler than the implementation. Databases and file systems are
| good examples. A database can be specified as giant arrays with
| linear search. Now prove that the database with all its
| optimizations and concurrency behaves the same as the simple
| spec.
| SubjectToChange wrote:
| Using (formal) specification languages doesn't guarantee a
| specification is "correct" either.
|
| _You have to write more code, and in a different language, but
| unlike just testing you can actually prove that invariants hold
| for all possible inputs._
|
| Formal verification is needed to show that the code actually
| implements a specification. If anything, a formal specification
| is really good for _generating_ test suites for the
| implementation code.
| yodsanklai wrote:
| I learned recently that the Coq project was renamed Rocq
| https://rocq-prover.org.
| rafram wrote:
| Probably the right move.
| bigstrat2003 wrote:
| Definitely not the right move. The old name was perfectly
| fine and allowed for harmless fun. They can obviously do what
| they wish, but IMO there's no good reason to destroy good
| clean fun just because it might upset the occasional person.
| lelandfe wrote:
| Not even a wink or a nudge about why they renamed:
| https://rocq-prover.org/about#Name
| SubjectToChange wrote:
| The linked discussion is upfront about the name change, if it
| wasn't already obvious.
|
| https://coq.discourse.group/t/coq-community-
| survey-2022-resu...
| lelandfe wrote:
| Ah, the community voted on it. The reason why the survey
| was proposed shall, however, remain a mystery.
| jghn wrote:
| I was not part of the survey but count me as someone who
| felt concern whenever I had to say it in a public or
| professional setting.
| lsuresh wrote:
| Related: Verus (verified Rust): https://github.com/verus-
| lang/verus
|
| It's aimed more at full systems verification (been used to build
| verified filesystems, kubernetes controllers etc...).
___________________________________________________________________
(page generated 2025-03-17 23:00 UTC)