Besides from Haskell (after all, Haskell is named after Haskell Curry), or academic languages like Agda, Idris, or Coq, which of the current programming languages, specially the ones that have some real-world applications, can be used to write programs that would be isomorphic to proofs?