The proof checking feature makes dependently typed languages closely related to proof assistants.
Η δυνατότητα ελέγχου αποδείξεων καθιστά τις γλώσσες με εξαρτώμενους τύπους στενά συνδεδεμένες με βοηθούς αποδείξεων.