Actually they use OCaml for the blockchain implementation and their own functional and provable language "Michelson" for smart contracts.

Fun fact: Michelson was the guy that disproved aether :)