Idris and Lean have a similar advantage; once you get past the general notation, the code syntax is very smooth and easy to follow.