Skip to content

Commit cd6efdf

Browse files
committed
mention languages with first-class contracts
1 parent 38d5f6a commit cd6efdf

1 file changed

Lines changed: 5 additions & 1 deletion

File tree

README.md

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -178,7 +178,11 @@ Anodized differentiates itself with a few key design choices:
178178

179179
Older crates like `libhoare` (a compiler plugin from before procedural macros were stabilized) and `dbc` explored similar ideas, proving the long-standing interest in Design by Contract within the Rust community. Anodized benefits from the modern procedural macro system, which allows for much better integration with the compiler and toolchain.
180180

181-
**Language-Level Discussions**
181+
**Inspiration from Other Languages**
182+
183+
Anodized is also inspired by languages where contracts are a first-class feature, not just a library. Languages like [Whiley](https://whiley.org), [Eiffel](https://eiffel.org), and [Ada/SPARK](https://adacore.com/about-spark) demonstrate the power of deeply integrating formal specifications into the type system and toolchain. While Anodized is a library, it aims to bring a similar level of integration and ergonomic feel to the Rust ecosystem.
184+
185+
**Towards First-Class Contracts for Rust**
182186

183187
There have been official discussions and RFCs within the Rust project itself about adding native support for contracts to the language. Anodized is designed to be a practical, library-based solution that can be used **today**, while also serving as a testbed for ideas that could inform future language-level features.
184188

0 commit comments

Comments
 (0)