3 ms·

yes. tests test what? logic. logic = types (proven). so stronger type system less test needs to be written. more, if proc macro or build.rs can execute logic,

yes. tests test what? logic. logic = types (proven). so stronger type system less test needs to be written. more, if proc macro or build.rs can execute logic, based on parsed """types"""(partial info only), we can extend type systems with custom logic (and panic at compile time and/or startup time if usage violation detected). on top of that, add fail fast (fail at compile time, build time or start up time) and newtype and errors-part-of-api culture; and lack of late binding (dyn is very limited use, no runtime reflection), and we get even less reasons to write tests. some examples of industrial """typing"""(eDSLs, construction time) solutions in rust : - https://github.com/elastio/bon https://github.com/elastio/bon - https://github.com/contextgeneric/cgp https://github.com/contextgeneric/cgp - https://github.com/paritytech/orchestra https://github.com/paritytech/orchestra - https://git.pipapo.org/cehteh/linear_type.git https://git.pipapo.org/cehteh/linear_type.git sure we need write tests, and tests like antithesis helps with. but list of tools helping with tests exactly as antithesis does(and more of others) is huge. that is built on top of absolutely strong supply chain audit, quality and security. there is even """levels""" of determinism tooling to decide how much to pay for cloud compute.

vlovich123 1y ago
Ok. Please write me an implementation of RAFT using no tests and have the Rust type checker prove correctness. I admit complete ignorance into how to get Rust to even go about partially proving that.
- dlahoda 1y ago
  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.
- lmm 1y ago
  Encode the relevant parts of the specification into the type system. E.g. if the specification says that you must only call A after you've called B and C, make B and C return some unique token type (with zero size at runtime) and make A require a parameter of that token type.

vlovich123 1y ago

Ok. Please write me an implementation of RAFT using no tests and have the Rust type checker prove correctness. I admit complete ignorance into how to get Rust to even go about partially proving that.

dlahoda 1y ago
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.
lmm 1y ago
Encode the relevant parts of the specification into the type system. E.g. if the specification says that you must only call A after you've called B and C, make B and C return some unique token type (with zero size at runtime) and make A require a parameter of that token type.