Arend

As a programming language enthusiast, continuously following the news in this topic : i thought i would know about any ongoing serious project of good programming language development. And sneaky JetBrains proved me wrong. All from nowhere they suddenly announce Arend 1. Arend seems to me to be a very professionally designed programming language. With very modern type system ["homotopy"]. To give you some reference : not even F* or Idris 2 are going to support homotopy type theory, at least according to my poor knowledge. The closest competitor of Arend is Microsoft's Lean and Agda. Being JetBrains we expect good IDE support for it. And we would be right, as the IDE already now, at the start is perhaps the best among well designed programming languages. Too fantastic to be true? Yes. It has a tiny deficiency : it is not designed to create executables, one can not execute Arend programs. It is only for modelling and verification. Yet. But i am still very happy about this development, as i am very optimistic that executability will come to Arend over time and i interpret this development as one more stepping stone towards modern programming. With this JetBrains is only the second firm to have created a professionally designed programming language with powerful type system, Microsoft being the first perhaps with F* and Lean.