It's a rather traditional type system; the specification is here: http://software.rochus-keller.ch/busy_spec.html. The main advantage are the combination of modularization, types and formal declarations, so that if you make a change in a large build (such as my https://github.com/rochus-keller/LeanQt or https://github.com/rochus-keller/LeanCreator systems) incompatibilites are immediately found by the compiler. Without these features you can never be sure whether all effects were checked.