 Matita adopts a tactic-based editing mode; (XML-encoded) proof objects are produced for storage and exchange.Existential variables are native in Matita, allowing a simpler management of dependent goals.Matita implements a bidirectional type inference algorithm exploiting both inferred and expected types.