I'm looking for the best formal language, where "best" implies elegance, simplicity and consistency.
It doesn't have to be a programming language, although I'm expecting most candidates to be. Mathematics, RDF/OWL and lojban are examples of non-programming languages that could be acceptable candidates.
One way to gauge how good a language is could be to compare how it solves some of the usual programming challenges such as Project Euler and TodoMVC against other languages.
For example, it seems like a logic programming language like Prolog would excel at Project Euler, while a FRP language/framework like Elm would excel at TodoMVC.
Please note that I do not care at all about pragmatism. The language could exist without a compiler, be abandoned, have no community or third-party packages/modules, take 1 year to execute Project Euler's Problem 1, etc.
I'm more interested in the discussion and process than in finding what the actual "best" language is.
- It is an ML family language, with a compiler written in Haskell. This comes with all the elegance and clean syntax of a modern typed functional language.
- It uses a dependent type system, similar to Agda. This means that the types can carry arbitrary proof information.
- The infrastructure is built around this. There is a proof assistant to assist you in building proofs that everything works.
- Its not entirely unpragmatic, as it actually has a (small) community, and can compile to C and then (somewhat) efficient code. But who cares about that, right?
For a really cool example, see this video, where they implement a Semigroup and Monoid instance for an Option type, including proofs that the appropriate laws hold for the implementation: https://www.youtube.com/watch?v=P82dqVrS8ik