Agda is a functional programming language with built-in support for dependent types. A dependent type depends on a value. This allows the developer to specify strict constraints for the types used in an application. Writing code with dependent types results in fewer type-related errors slipping through the compilation process.
When executing Agda code, it is first compiled into a different programming language. This process is called code extraction. This step is applied since most of the typed code becomes unnecessary after type-checking and can therefore be removed. Currently, the Agda compiler supports only Haskell and JavaScript as target languages. However, exploring Rust as a target language could potentially lead to better performance, and it would allow access to the Rust library ecosystem.
Overall, the agda2rust backend could be a viable alternative to what is currently available. While it is not fully feature-complete and will not outperform any existing backends yet, agda2rust provides a way to seamlessly integrate algorithms and data structures implemented and proven in Agda into an existing Rust codebase.