HNC Competitors and Non-Competitors

In the long run HN0 is going to be only a bottom layer in a full-fledged language.

With High Level Typed Targets

The need to have typed targets puts architectural restrictions on type checker and optimizer. The checker has to remember types of subterms, and optimizer has to construct type annotations.

• Purescript
• HaXe
• Vala
• Felix
• Mercury
• Futhark
• JSCaml
• Argile

Without High Level Typed Targets

• Om
• Rust
• Typescript
• Koka
• ThinScript
• Roy
• Morte
• Fable
• Infernu
• Lasca
• Oczor

Proof Systems

These languages represent our final destination. While they direct our development, their code generation capabilities can be largely ignored at this early stage.

• Exe
• Ditto
• Hubris
• Idris
• Agda
• Coq
• Lean
• ATS - uses a decidable arithmetic to prove static assertions
• Dedukti
• pi-forall
• sconybeare/mltt - MLTT checker in Haskell
• F* - uses an SMT solver to prove static assertions
• Hoq - JetBrains
• Cubical
• Reliquary - a dependently typed concatenative languages

Unrelated

• zot_haskell - minimalistic Zot language implemented in Haskell
• eolang
• Eff
• Impala
• Lol - Lisp on Erlang
• Eta - GHC backend for JVM
• Ohm - Alan Kay's exercise in compact design
• hakaru
• latro