Ask HN: What's the best formal language? | Hacker News Reader

Ask HN: What's the best formal language?

9 pointsmiguelrochefort6 comments

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.

Consider Idris. http://www.idris-lang.org/

- 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

Most formal languages are created with an specific purpose, so there isn't simply a "best" one. You normally use tons of them in academia, and many times simultaneously.

If you give more information about what you are looking for, we may be able to help you.

If you just want to learn something interesting though, I'd say typed lambda calculus is a great option.

The simply typed lambda calculus.

The lambda calculus

Good suggestion. Also consider its programming language counterpart, Scheme.

Scheme is like untyped calculus.

What about typed calculus?

Reply on news.ycombinator.com