Rendered at 19:38:14 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
63 6 hours ago [-]
If you found this interesting, you may also be interested to hear about some related projects with similar goals/scopes: Miri[0], Kani[1], and Creusot[2]. There looks to be some significant overlap between Verus, Kani, and Creusot but I've not used any of them so I'll refrain from trying to differentiate them.
Miri: proves pre-defined properties, no changes to code other than adding a few annotations
Kani: use in a test suite
Creusot: annotations
Verus: annotations or macro
The macro system looks very nice if it doesn't slow down the normal build.
gregwebs 35 minutes ago [-]
AI tells me that code using the verus! macro everywhere would double in build time but if only used ocassionally the verus! macro would only increase build time by a few percent. The attribute annotation would basically be free, but there is a downside that loop invariants would be rejected by stable rustc.
reddit_clone 27 minutes ago [-]
This is very interesting.
I am new to Rust and also new to formal verification.
Can someone ELI5 this for me?
(Also, when does the proof happen? During compilation or by running extra tests during unit testing?)
sourdecor 17 hours ago [-]
Verus seems to be exactly what I have been looking for! I discovered AllConcur[0] on HN a while back, and I wanted to port it to Go, but since it used TLA+ and C, and it was very confusing for me to understand how you can trust the implementation unless you can compile TLA+ to C.
I was talking to Gemini about comparing Verus to TLA+ and it said that TLA+ is usually used (for example) "to prove that a distributed consensus protocol is logically sound" but when I asked if Verus can do that too, it said yes. So Verus can be compiled and integrated with Rust, whereas TLA+ is used more for blueprint development that then guides the implementation in the mind of the implementer.
That is my pet peeve against TLA+ advocacy, the disassociation between a theoretical proof of a specific algorithm, data structures, and the actual implementation in production.
I rather push for tooling that allows code generation based on the formal proofs like FStart or Dafny, or is integrated with specific programming languages like SPARK, Frama-C or this Verus.
igornotarobot 10 hours ago [-]
You can write everything in Lean and generate an implementation. Given that LLMs can now generate Lean proofs, this does not seem to be prohibitively expensive anymore. The real issue with distributed algorithms is that they are hard to reason about, and reasoning about them at the code level does not make the verification problem easier, it makes it harder.
jgalt212 8 hours ago [-]
> as very confusing for me to understand how you can trust the implementation unless you can compile TLA+ to C.
Preach. I feel like I'm taking crazy pills every time someone claims TLA+ as the sine qua non of provably correct systems. They should sub probably for provably.
zozbot234 6 hours ago [-]
There is no contradiction here, TLA+ is mostly about proving properties of toy models, not end-to-end proofs about real programs. As TLA+ practitioners like to point out, the latter is only applicable to favorable "local" properties - this is what type systems do, they state claims that are quite aligned with the program's syntactic structure; or else to rather trivial programs where proving "whole-program" claims is still feasible. Even Verus itself doesn't really change this.
japgolly 15 hours ago [-]
[dead]
freethinky 4 hours ago [-]
Does anyone now if something like this exist and is used (and actively maintained) for .NET/C#, not like Dafny where I write in another language (unlikely my company would allow that). Also as annotations (likely that I can start with it).
I have long been critical of verification tools requiring annotations. Humans cannot write correct code, so asking them to write correct proof annotations seems futile.
But maybe this changes in the age of LLMs. A deterministic check to let LLMs verify the correctness of an API could improve the success rate of large scale refactors or performance optimizations.
Exciting!
afdbcreid 4 hours ago [-]
You seem to have misunderstood the idea. The entire idea of proof annotations is that they are not manual. Rather, the verifier checks you fulfill the preconditions for the method you calls, and it checks inside the method that if the preconditions are fulfilled then the postconditions are too. This just helps the verifier reason locally. At the end besides more burden, the only thing you really need to check is the top-level annotations, like any formal verifier.
MeetingsBrowser 3 hours ago [-]
> the only thing you really need to check is the top-level annotations
Sorry if I wasn’t clear.
My point is that the annotations are manual and inherently prone to error.
If humans could correctly write annotations according to a spec, we wouldn’t need verifiers at all. We could just write correct code directly.
There is an argument to be made that the annotations are a smaller surface than full blown code and therefore easier for humans to reason about.
However, in practice formal verification tools and annotations are far more obscure than regular code.
Thousands of people write and review code both professionally and as a hobby. But most people writing verifier annotations have a PhD in some field adjacent to formal verification.
rcxdude 2 hours ago [-]
the vast majority of such annotations are checked though. There's generally three kinds of annotations in formal proof systems: assertions about inputs that cannot be checked by the system, statements of propositions that want to be checked, and proofs that those propositions follow from the assertions. The proofs are checked by the system, so writing them is mainly just tedious and difficult, not really a source of error. What needs to be verified carefully is that the assertions are true, and that the propositions actually correlate with what people actually want out of the system. The mark of how effective a formal verification system is is in how strong of a proposition can be proven from how small a set of assertions. (well, and then how difficult it is to write the proofs).
rzmmm 1 hours ago [-]
I think it provides best bang for buck when the annotation is "obviously correct" but the implementation is complex.
For example if you are trying to prove that your new sorting algorithm yields sorted list for all inputs.
If there is as much annotations as there is code, then testing is better tool for the job than verification.
nottorp 9 hours ago [-]
Would it help with the bugs in the new and improved ubuntu coreutils?
Betelbuddy 6 hours ago [-]
It will prove the bugs were corrected implemented... :-) And that your mistaken specification of the tax rules in Switzerland, was correctly translated to code, and that your mistaken specification of the process to request a mortgage is mathematically valid...and that your wrong logic about how much centrifugal force your rocket will be able to stand on ascent was mathematically translated to proven correct code running the incorrect logic...
naive applications of this would lead you to believe no knowledge is possible, and that progress is not meaningful when liveness can’t be guaranteed.
it’s all rubbish, grandparent is a small mind who can’t figure out how it’s a step up from nothing.
svieira 3 hours ago [-]
I wouldn't say it's all rubbish - it's very easy for someone new to theorem proving to presume the equivalent of "strong typing will eliminate the possibility of errors", but the more correct understanding is "strong typing will reduce the number of things you have to keep in your head at any one time thus reducing the possibility of errors".
nottorp 18 minutes ago [-]
The thing with ubuntu's rust coreutils is that they, for example, crash when told to recurse because they use actual recursive calls to go into subdirs and run out of stack space if the structure is big enough.
What formal correctness proof will detect that?
Jtsummers 3 hours ago [-]
I presume you also can't stand people who write software tests for similar reasons? The test is wrong, the code is wrong. The spec is wrong, the code is wrong. What a waste of effort! Just write correct code people! Verification is left as an exercise for the end users. Who cares about them anyways? /s
Betelbuddy 3 hours ago [-]
Testers are not selling guarantees...
rcxdude 2 hours ago [-]
Tests are guaranteeing that the product doesn't fail under the test conditions. Formal verification is guaranteeing the product doesn't deviate from the formal spec under a given set of assumptions. Both of them are useful but depend on how well the thing being checked actually correlates with what you care about.
Betelbuddy 1 hours ago [-]
Interesting definition of guarantee....what about the people who run millions of them? Well Microsoft: "AS IS." Apple: "WITH ALL FAULTS" Adobe: "no guarantee of error-free operation."
Apparently their lawyers never got the memo that the tests already guaranteed the software...
rcxdude 26 minutes ago [-]
Well yeah, why would they offer an legal guarantee if they don't have to? They could have a watertight proof that their software works perfectly in all situations (lol) but the lawyers still would prefer to disclaim as much liability as possible.
And even if they did, all the test guarantee is that the tests pass, of course the main limit is that they don't actually test even a small fraction of what the customers actually want to do.
Jtsummers 2 hours ago [-]
That's exactly what testers are selling though. If they aren't guaranteeing the program is correct (up to what is tested) then what purpose do they serve? Same with formal methods, offering guarantees up to what is proven.
Betelbuddy 2 hours ago [-]
Oh my my...
"Program testing can be used to show the presence of bugs, but never to show their absence"
- Edsger Dijkstra
Jtsummers 2 hours ago [-]
Ah, but you can't stand those formal methods folks, why are you appealing to authority with Edsger Dijkstra?
Betelbuddy 1 hours ago [-]
You are trying to convince me that because you pressed "A" once on the vending machine and worked, you declare "A" is proven to dispense Coke...
Jtsummers 1 hours ago [-]
> You are trying to convince me that because you pressed "A" once on the vending machine and worked, you declare "A" is proven to dispense Coke...
This thread is hilarious, thank you. You start off saying you "cant [sic] stand formal methods people" and now you're giving an example of why formal methods are useful. And you're appealing to authority using a man who was a major proponent of formal methods. What's your actual position on formal methods?
Betelbuddy 44 minutes ago [-]
Have you considered a career is stand up comedy?
The quote from Dijkstra stands on its own...quoting a famous person stating something independently demonstrable, does not magically turn the statement into an appeal to authority :-))
>> a man who was a major proponent of formal methods.
No he was not, but you see, its irrelevant in the context of the argument you failed to defend. And Dijkstra fails your purity test.
He himself wrote that he saw "no specific virtue in being a formalist" and would use formal methods "when I feel they help."
lukeify 9 hours ago [-]
Reminds me of Whiley, which was developed by one of my university professors.
That's fascinating. Does it mean it verifies mathematical proofs directly within the Rust code? Does anyone know the underlying principles of how this is possible?
Jtsummers 16 hours ago [-]
https://verus-lang.github.io/verus/publications-and-projects... - The papers here go into their implementation. They take the proof statements and information about the program and turn it into an SMT problem (and run it through Z3 if I read correctly) and then they use that to prove the properties of the program.
SPARK/Ada and Dafny work similarly, and have good documentation if you want to try your hand at something with a (presently) better set of documentation.
All it does is dispatch proof obligations to an SMT solver like Z3. There is nothing special about Verus, it works in the same way other program verification frameworks like Dafny and Frama-C work - except it's for Rust.
Most of this article presents nothing unique to Verus and is more of an advertisement for the authors research work and the other work AWS is doing.
anonymousDan 7 hours ago [-]
I like how they also neglected to mention that Verus was invented at Microsoft...
hwayne 6 hours ago [-]
Not the first time Microsoft employees invented a formal methods tool, Microsoft ignored them, and AWS scooped them up. Not the second or third time, either.
anonymousDan 5 hours ago [-]
I don't think it's entirely fair to say they ignored them. As far as I know they are still employed at Microsoft Research and working on developing and improving the tool?
canadiantim 16 hours ago [-]
This seems like a big deal
m00dy 10 hours ago [-]
I just read the whole thing, the post would be even better if it includes an example for concurrency. It's not easy to imagine it just by looking at the binary search's example.
Ive been using Rust with LLMs for the past 2 years already. It's just amazing, I can't really think anything else to code with. Normally, been testing my codes unit tests + integration tests where necessary. But, I will take a look at this seriously.
m00dy 11 hours ago [-]
>>The result is fast code that's more correct and secure than average.
Welcome to Rust
kobahiro 17 hours ago [-]
[flagged]
jongjong 15 hours ago [-]
What if the 'mathematical specification of its functionality' is incorrect? How to prove the correctness of the mathematical specification faster than the underlying environment, code and dependencies change?
IMO, formal verification is never going to work. It's very clear that a lot of people are desperate to see it used in mainstream software development, but every innovation which proponents have seen as an opportunity to finally prove its utility has only served to further discredit it.
Now proponents are at a point that they literally have to convince us that people who aren't able to write correct code are somehow able to write correct mathematical specifications!
This is quite an extraordinary claim given that the mathematical specification is an order of magnitude longer and more complex than the code itself... And every experienced software engineer knows that mistakes grow proportionally to the size of the logic... Unfortunately, mathematical spec is logic; just like code, except it's more complex and thus more error-prone.
And don't even get me started on the fact that APIs, engines and languages change constantly from under you and thus the mathematical spec would get completely invalidated every week or so each time you did an update. Unfortunately, even in the best case scenario, reality is always going to change and invalidate our proofs faster than we can publish them. By the time you've proven the theory, its underlying assumptions already ceased to hold true.
Even in a far simpler hypothetical world with just one piece of software; the software's own execution could potentially change the reality which it relied on to prove its own correctness and would thus invalidate its own correctness merely by executing.
gr_norm 15 hours ago [-]
> How to prove the correctness of the mathematical specification?
You can show that your specifications satisfy well-accepted criteria like confidentiality and integrity. This is usually done as the final verification step. For example, AWS just did it for the Nitro hypervisor used by EC2: https://aws.amazon.com/blogs/compute/aws-nitro-isolation-eng....
stevenhuang 15 hours ago [-]
So it moves from both "my implementation and specification is incorrect", to just "my specification is incorrect".
I don't understand this type of thinking. Proving what you can is still better. Don't let perfect be the enemy of good.
jongjong 13 hours ago [-]
>> Don't let perfect be the enemy of good.
I feel like the exact same line could be used to argue the opposite point against formal verification.
I'm not saying that proof is inherently bad. If it was free, then I agree it would be good, but my point is that it's not free. Proofs are expensive to produce, maintain, they lock-down flawed implementations, focus on correctness but disregard more important aspects like modularity (I.e. loose coupling, high cohesion). Also; formal proofs discourage change and they create false confidence about reliability because sometimes the bug is in the spec itself, especially as the spec gets more complicated.
I think modularity is a more useful property to aim for in terms of achieving the right degree of correctness over the life of the software, in a practical sense.
Formal proofs can work against modularity if the proof must be rewritten in order to achieve modularity as requirements change over time; which is the reality for most software.
imtringued 6 hours ago [-]
Nothing forces developers to write a complete specification of the algorithm. You want to have it both ways.
If developers keep the spec concise but incomplete, then you say the spec is incorrect so now you have to prove that the spec is correct. Ok, but people already use unit tests to sample the behaviour of a function so they already accept some degree of inaccuracy. By your logic you have to enumerate the entire input space otherwise unit testing is worthless.
If developers decide to build a complete specification of the algorithm, you counter that the specification is now too long so they should not bother.
You are basically arguing with yourself.
The update argument doesn't make sense either, because you generally want to prove properties like absence of panics throughout your entire codebase. Again this is just a roundabout way of arguing against the very idea of a tradeoff.
atoav 11 hours ago [-]
That means when one goes out of whack, someone will notice. E.g. let's say the mathematical property is correct, but someone optimizes some behavior. Without tests or verification that could break production or worse: not break it, but break security without anybody noticing.
That is worth the hassle for some applications.
lou1306 10 hours ago [-]
> people who aren't able to write correct code are somehow able to write correct mathematical specifications
This describes about one or two thirds of the Theoretical CS academic community (conservative estimate) /s
> This is quite an extraordinary claim given that the mathematical specification is an order of magnitude longer and more complex than the code itself
I find this hard to believe. The mathematical specification for "array a is sorted" is "forall n in Nat: 0 < n < len(a) -> a[n] >= a[n+1]". The average sorting algorithm is usually a tad longer than this.
> the mathematical spec would get completely invalidated every week or so each time you did an update
Well of course nobody serious advocates for formalizing/verifying code that is subject to that much churn (be it internal or external).
bcjdjsndon 7 hours ago [-]
> With Verus, however, developers can mathematically prove the safety of their unsafe Rust code, re-establishing machine-checked safety guarantees
Why then does rust even need the unsafe keyword?
afdbcreid 4 hours ago [-]
Because Rust is not Verus, and not all unsafe code needs formal-verification-level of rigorousness. Also, there are other verifiers as well.
hwayne 5 hours ago [-]
There's a huge difference between "Verus can prove the safety of unsafe code" and "Verus can EASILY prove the safety of unsafe code." And I bet it can't prove everything, like calls to a C ABI.
ijustlovemath 6 hours ago [-]
I'd rather have all the unsafe code scoped and the safety invariants explained than the alternative. You still can't do a whole class of scary things in an unsafe block; common misconception
bsaul 6 hours ago [-]
That's indeed a weird feeling when going back to another language after having coded in rust. First you're happy not having to write any "unsafe" keyword. Then you're horrified for the very same reason.
bcjdjsndon 4 hours ago [-]
Yeah but if this program can prove unsafe code is safe... Why can't rust compiler do it, and hence, why do we even need unsafe if the compiler can do it.
ijustlovemath 2 hours ago [-]
It generates additional code that's fed into an SMT solver. Poor compiler performance is a top issue developers have with Rust, which they're working to solve. I think adding this layer into every piece of code (which is probably impossible since inferring the invariants is essentially inferring your business logic) would eat away gains they've achieved.
I also think the functional style, typestate, and borrow checker is enough for writing correct code across many business domains, so there's no need to add this to your toolchain. We are a med device company building a class III (really 3 class II) device, and Verus is making our verification story extremely compelling.
Jtsummers 3 hours ago [-]
> Yeah but if this program can prove unsafe code is safe... Why can't rust compiler do it
This question only makes sense if you think Verus is part of the Rust compiler. It's not. And even if it were, the additional annotations are still required to prove that the unsafe block is actually safe. So this could, if integrated into the Rust compiler, help programmers eliminate some unsafe blocks (perhaps even most), but likely not all, and not without additional code proving that the section is safe.
Meneth 9 hours ago [-]
"Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth.
112233 7 hours ago [-]
> With Verus, however, developers can mathematically prove the safety of their unsafe Rust code
what about proving safety of not-unsafe code? The meme that rust is "safe" is becoming tiring. Does this thing allow proving absence of infinite loops? Bounded resource use? Correctness of comparison operations? Etc.
Also, why is there still no hardware tagging to simply prevent memory misuse at cpu level, if it actually is such an important issue?
ijustlovemath 6 hours ago [-]
What exactly is your objection? Rust doesn't solve the halting problem? You can absolutely prove bounded resource use with eg SmallVec and arenas
[0]https://github.com/rust-lang/miri
[1]https://github.com/model-checking/kani
[2]https://github.com/creusot-rs/creusot
Kani: use in a test suite
Creusot: annotations
Verus: annotations or macro
The macro system looks very nice if it doesn't slow down the normal build.
I am new to Rust and also new to formal verification.
Can someone ELI5 this for me?
(Also, when does the proof happen? During compilation or by running extra tests during unit testing?)
I was talking to Gemini about comparing Verus to TLA+ and it said that TLA+ is usually used (for example) "to prove that a distributed consensus protocol is logically sound" but when I asked if Verus can do that too, it said yes. So Verus can be compiled and integrated with Rust, whereas TLA+ is used more for blueprint development that then guides the implementation in the mind of the implementer.
Seems awesome!
[0]: https://news.ycombinator.com/item?id=12357976
I rather push for tooling that allows code generation based on the formal proofs like FStart or Dafny, or is integrated with specific programming languages like SPARK, Frama-C or this Verus.
Preach. I feel like I'm taking crazy pills every time someone claims TLA+ as the sine qua non of provably correct systems. They should sub probably for provably.
But maybe this changes in the age of LLMs. A deterministic check to let LLMs verify the correctness of an API could improve the success rate of large scale refactors or performance optimizations.
Exciting!
Sorry if I wasn’t clear.
My point is that the annotations are manual and inherently prone to error.
If humans could correctly write annotations according to a spec, we wouldn’t need verifiers at all. We could just write correct code directly.
There is an argument to be made that the annotations are a smaller surface than full blown code and therefore easier for humans to reason about.
However, in practice formal verification tools and annotations are far more obscure than regular code.
Thousands of people write and review code both professionally and as a hobby. But most people writing verifier annotations have a PhD in some field adjacent to formal verification.
For example if you are trying to prove that your new sorting algorithm yields sorted list for all inputs.
If there is as much annotations as there is code, then testing is better tool for the job than verification.
Jesus, I cant stand formal methods people...
it’s all rubbish, grandparent is a small mind who can’t figure out how it’s a step up from nothing.
What formal correctness proof will detect that?
Apparently their lawyers never got the memo that the tests already guaranteed the software...
And even if they did, all the test guarantee is that the tests pass, of course the main limit is that they don't actually test even a small fraction of what the customers actually want to do.
"Program testing can be used to show the presence of bugs, but never to show their absence"
This thread is hilarious, thank you. You start off saying you "cant [sic] stand formal methods people" and now you're giving an example of why formal methods are useful. And you're appealing to authority using a man who was a major proponent of formal methods. What's your actual position on formal methods?
The quote from Dijkstra stands on its own...quoting a famous person stating something independently demonstrable, does not magically turn the statement into an appeal to authority :-))
>> a man who was a major proponent of formal methods.
No he was not, but you see, its irrelevant in the context of the argument you failed to defend. And Dijkstra fails your purity test.
He himself wrote that he saw "no specific virtue in being a formalist" and would use formal methods "when I feel they help."
SPARK/Ada and Dafny work similarly, and have good documentation if you want to try your hand at something with a (presently) better set of documentation.
https://mitpress.mit.edu/9780262546232/program-proofs/ - Dafny book, pretty good tutorial on the topic
https://learn.adacore.com/courses/intro-to-spark/chapters/01... - Free tutorial for SPARK
Welcome to Rust
IMO, formal verification is never going to work. It's very clear that a lot of people are desperate to see it used in mainstream software development, but every innovation which proponents have seen as an opportunity to finally prove its utility has only served to further discredit it.
Now proponents are at a point that they literally have to convince us that people who aren't able to write correct code are somehow able to write correct mathematical specifications!
This is quite an extraordinary claim given that the mathematical specification is an order of magnitude longer and more complex than the code itself... And every experienced software engineer knows that mistakes grow proportionally to the size of the logic... Unfortunately, mathematical spec is logic; just like code, except it's more complex and thus more error-prone.
And don't even get me started on the fact that APIs, engines and languages change constantly from under you and thus the mathematical spec would get completely invalidated every week or so each time you did an update. Unfortunately, even in the best case scenario, reality is always going to change and invalidate our proofs faster than we can publish them. By the time you've proven the theory, its underlying assumptions already ceased to hold true.
Even in a far simpler hypothetical world with just one piece of software; the software's own execution could potentially change the reality which it relied on to prove its own correctness and would thus invalidate its own correctness merely by executing.
You can show that your specifications satisfy well-accepted criteria like confidentiality and integrity. This is usually done as the final verification step. For example, AWS just did it for the Nitro hypervisor used by EC2: https://aws.amazon.com/blogs/compute/aws-nitro-isolation-eng....
I don't understand this type of thinking. Proving what you can is still better. Don't let perfect be the enemy of good.
I feel like the exact same line could be used to argue the opposite point against formal verification.
I'm not saying that proof is inherently bad. If it was free, then I agree it would be good, but my point is that it's not free. Proofs are expensive to produce, maintain, they lock-down flawed implementations, focus on correctness but disregard more important aspects like modularity (I.e. loose coupling, high cohesion). Also; formal proofs discourage change and they create false confidence about reliability because sometimes the bug is in the spec itself, especially as the spec gets more complicated.
I think modularity is a more useful property to aim for in terms of achieving the right degree of correctness over the life of the software, in a practical sense.
Formal proofs can work against modularity if the proof must be rewritten in order to achieve modularity as requirements change over time; which is the reality for most software.
If developers keep the spec concise but incomplete, then you say the spec is incorrect so now you have to prove that the spec is correct. Ok, but people already use unit tests to sample the behaviour of a function so they already accept some degree of inaccuracy. By your logic you have to enumerate the entire input space otherwise unit testing is worthless.
If developers decide to build a complete specification of the algorithm, you counter that the specification is now too long so they should not bother.
You are basically arguing with yourself.
The update argument doesn't make sense either, because you generally want to prove properties like absence of panics throughout your entire codebase. Again this is just a roundabout way of arguing against the very idea of a tradeoff.
That is worth the hassle for some applications.
This describes about one or two thirds of the Theoretical CS academic community (conservative estimate) /s
> This is quite an extraordinary claim given that the mathematical specification is an order of magnitude longer and more complex than the code itself
I find this hard to believe. The mathematical specification for "array a is sorted" is "forall n in Nat: 0 < n < len(a) -> a[n] >= a[n+1]". The average sorting algorithm is usually a tad longer than this.
> the mathematical spec would get completely invalidated every week or so each time you did an update
Well of course nobody serious advocates for formalizing/verifying code that is subject to that much churn (be it internal or external).
Why then does rust even need the unsafe keyword?
I also think the functional style, typestate, and borrow checker is enough for writing correct code across many business domains, so there's no need to add this to your toolchain. We are a med device company building a class III (really 3 class II) device, and Verus is making our verification story extremely compelling.
This question only makes sense if you think Verus is part of the Rust compiler. It's not. And even if it were, the additional annotations are still required to prove that the unsafe block is actually safe. So this could, if integrated into the Rust compiler, help programmers eliminate some unsafe blocks (perhaps even most), but likely not all, and not without additional code proving that the section is safe.
what about proving safety of not-unsafe code? The meme that rust is "safe" is becoming tiring. Does this thing allow proving absence of infinite loops? Bounded resource use? Correctness of comparison operations? Etc.
Also, why is there still no hardware tagging to simply prevent memory misuse at cpu level, if it actually is such an important issue?