Comment by armchairhacker

Theorem proving and complex types are like extensions on an otherwise ordinary language:

- Agda, Idris, etc. are functional languages extended with complex types

- Isabelle, Lean, etc. are functional languages extended with complex types and unreadable interactive proofs

- Dafny etc. are imperative languages extended with theorems and hints

- ACL2 is a LISP with theorems and hints

Related, typeclasses are effectively logic programming on an otherwise functional/imperative language (like traits in Rust, mentioned in https://rustc-dev-guide.rust-lang.org/traits/chalk.html).