3 ms·

you cannot prove RAFT correctness using Rust type checker. wdym by "no tests"? seems you have not read my response at all... > sure we need write tests, and

you cannot prove RAFT correctness using Rust type checker. wdym by "no tests"? seems you have not read my response at all... > sure we need write tests, and tests like antithesis helps with. also, imho both lamports (bft and paxos) and are better of raft https://www.hytradboi.com/2025/2016d6c4-b08d-40b3-af2f-67926ca8521f-enough-with-all-the-raft https://www.hytradboi.com/2025/2016d6c4-b08d-40b3-af2f-67926...

vlovich123 1y ago
Regardless of the algorithm, antithesis specifically can make sure your implementation is correct. You started this thread by claiming that that’s needed less in Rust because the type system helps you avoid bugs. I’m highlighting classes of problems that Antithesis is targeting to help you test and Rust’s type system cannot help you with. Raft vs Paxos doesn’t matter
- dlahoda 1y ago
  check this https://news.ycombinator.com/item?id=45264789 https://news.ycombinator.com/item?id=45264789 , antitesis feels like set of bash scripts thb
- dlahoda 1y ago
  1. many things antithesis finds in go, kotling, cpp just do not exist in rust. that i less needed case. these people like antithesis. 2. i mentioned tooling, also in other thread i mentioned ecosystem - https://github.com/BurtonQin/Awesome-Rust-Checker https://github.com/BurtonQin/Awesome-Rust-Checker - add link for dozen of tools for cfg feature(product lines) eng here (compile time conditional composeability) and const expressions - add link to dozen of tools to audit deps and decide on panic safety and first class crash hooks crates - mix with nix which many (way many compared to go, kotlin, cpp) rust projects use (and sri cargo.lock out box) - and qemu/mozilla/no rr tools (no determinism to get seed, and run slower hosts things w that seed) - and add here clusterfuzz eco (supports all oss fuzzers, and these do proper search https://camshaft.github.io/bolero/features/unified-interface.html https://camshaft.github.io/bolero/features/unified-interface..., and rust adapters allow for manual macro based fuzz narrowing in rust) - https://quint-lang.org/docs/model-checkers https://quint-lang.org/docs/model-checkers - several ongoing projects formalizing rust std and lang SO, why i need antithesis? To get Raft, will do sans-io with full typed rust covered by proofs for state(machine) and macro generator for glue(from state machine). I need only prop/fuzz test to test small integration sans-io part. I do not need antithesis.
  - vlovich123 1y ago
    Literally none of the things you mention help with verifying distributed systems. I think you just fundamentally aren't understanding what it is and this isn't the right forum for me to bridge that gap for you. You highlight this lack of understanding by dismissing a custom hypervisor as a collection of bash scripts and focusing on things Rust has or does well that are completely irrelevant for the classes of bugs that Antithesis is trying to uncover. > To get Raft, will do sans-io with full typed rust covered by proofs for state(machine) and macro generator for glue(from state machine). I need only prop/fuzz test to test small integration sans-io part. I do not need antithesis. Again, I think you're missing the point entirely. With hand written property test/fuzz test, you have to manually and correctly implement all the failure conditions that can happen "sans-io". A notable one would be packet reordering (if you're I/O doesn't guarantee ordering) or network partitions. The point of Antithesis is that it will transparently do all of that state checking for you. It's not that you'd not get there eventually, but Antithesis will be an easier system and you'll move faster. Whether or not that's valuable is a decision everyone makes for themselves.

vlovich123 1y ago

Regardless of the algorithm, antithesis specifically can make sure your implementation is correct. You started this thread by claiming that that’s needed less in Rust because the type system helps you avoid bugs. I’m highlighting classes of problems that Antithesis is targeting to help you test and Rust’s type system cannot help you with. Raft vs Paxos doesn’t matter

dlahoda 1y ago
check this https://news.ycombinator.com/item?id=45264789 https://news.ycombinator.com/item?id=45264789 , antitesis feels like set of bash scripts thb
dlahoda 1y ago
1. many things antithesis finds in go, kotling, cpp just do not exist in rust. that i less needed case. these people like antithesis. 2. i mentioned tooling, also in other thread i mentioned ecosystem - https://github.com/BurtonQin/Awesome-Rust-Checker https://github.com/BurtonQin/Awesome-Rust-Checker - add link for dozen of tools for cfg feature(product lines) eng here (compile time conditional composeability) and const expressions - add link to dozen of tools to audit deps and decide on panic safety and first class crash hooks crates - mix with nix which many (way many compared to go, kotlin, cpp) rust projects use (and sri cargo.lock out box) - and qemu/mozilla/no rr tools (no determinism to get seed, and run slower hosts things w that seed) - and add here clusterfuzz eco (supports all oss fuzzers, and these do proper search https://camshaft.github.io/bolero/features/unified-interface.html https://camshaft.github.io/bolero/features/unified-interface..., and rust adapters allow for manual macro based fuzz narrowing in rust) - https://quint-lang.org/docs/model-checkers https://quint-lang.org/docs/model-checkers - several ongoing projects formalizing rust std and lang SO, why i need antithesis? To get Raft, will do sans-io with full typed rust covered by proofs for state(machine) and macro generator for glue(from state machine). I need only prop/fuzz test to test small integration sans-io part. I do not need antithesis.
- vlovich123 1y ago
  Literally none of the things you mention help with verifying distributed systems. I think you just fundamentally aren't understanding what it is and this isn't the right forum for me to bridge that gap for you. You highlight this lack of understanding by dismissing a custom hypervisor as a collection of bash scripts and focusing on things Rust has or does well that are completely irrelevant for the classes of bugs that Antithesis is trying to uncover. > To get Raft, will do sans-io with full typed rust covered by proofs for state(machine) and macro generator for glue(from state machine). I need only prop/fuzz test to test small integration sans-io part. I do not need antithesis. Again, I think you're missing the point entirely. With hand written property test/fuzz test, you have to manually and correctly implement all the failure conditions that can happen "sans-io". A notable one would be packet reordering (if you're I/O doesn't guarantee ordering) or network partitions. The point of Antithesis is that it will transparently do all of that state checking for you. It's not that you'd not get there eventually, but Antithesis will be an easier system and you'll move faster. Whether or not that's valuable is a decision everyone makes for themselves.