I think humanity in general are only dimly aware of this space. The Research section is probably your best bet about what's different. I think your questions are what academics call "open".
The highlights seem to be:
- extensional equality (similar to nuprl)
- undecidable type-checking
- combination of both SMT and tactics, metaprogramming
- focus on compilation to mainstream languages, programming more than formalizing math