In short to give a confidence in correctness of a program that often exceeds that of other techniques (such as testing). More specifically, from the viewpoint o

In short to give a confidence in correctness of a program that often exceeds that of other techniques (such as testing). More specifically, from the viewpoint of a programmer there's three general ways that a language like this is useful. I'll use examples from this general class of languages (theorem provers) since Arend is still in its infant stages. 1. As a formalized specification language that allows you to engage in a dialog with the computer about what properties are entailed by such a specification. For example there is a team at Amazon that makes use of the language TLA+ to formally specify some AWS systems and use the computer to derive and check insights about those systems. This focus solely on the specification and ignores the code implementing the specification (this can still be extremely useful). This can also be used to verify the correctness of various CS algorithms. 2. As a language that can be used to check an implementation for conformance against a formal specification to provide a high degree of assurance they match. Examples of this include Isabelle for the microkernel seL4 (a recent post on HN) and Coq for the CompCert certified C compiler (apparently used by Airbus in some capacity and some other safety-critical industries). 3. As a language that can be directly used to generate code (or is in fact compiled/interpreted directly) and prove interesting properties about said code. There's a light version of languages like this in the form of languages like SPARK or analyzers on top of SystemVerilog Assertions, but these bear only a passing resemblance to something like Arend. They are, however, in use by essentially every big chip manufacturer and are widely used again in safety-critical industries. There are languages closer to Arend that try to accomplish something similar, such as again Coq and Isabelle (which allow for extraction of a runnable program in addition to being provers), but I'm not aware of high-profile usages of those. As far as I'm aware currently Arend is capable of doing the first. I'm not sure if it can do the second. I see no indication it can do the third. Crucially all this can be added later, potentially with little to no modification of the language. The third use case means in theory these languages (Coq, Isabelle, Arend, etc.) could be used to write ordinary programs. In practice few people do because it's very time-consuming, the tooling is subpar, and there isn't much of a community doing this. Arend is exciting to me because JetBrains could make a huge dent in the problems of tooling and community (see Kotlin). However, it's unlikely that even if JetBrains gave this its full support suddenly we'd have people writing ordinary web services with Arend. But it might just make other projects with high but not critical safety requirements (e.g. stuff like Kubernetes, Kafka, or at least small modules thereof) plausible to either verify or write directly with Arend.