It is far from solid and yet it is easy to understand (modulo corner cases) . I doubt that lambda-calculus-like language will take over it just because it gives one an ability to prove correctness properties in Coq.