El objetivo principal de este curso es introducir los asistentes de prueba como herramienta para definir estructuras matemáticas, para enunciar proposiciones sobre esas estructuras y probarlas formalmente. 


Se espera que quien tome este curso logre conocer las teorías subyacentes a diferentes asistentes de prueba y que pueda elegir uno que se adapte a la formalización que le interese hacer.


Quien apruebe el curso tendrá la capacidad para definir estructuras matemáticas (o computacionales), enunciar propiedades sobre ellas y probar teoremas en algún asistente; se fomentará el uso de las bibliotecas disponibles en el asistente en cuestión.


Se hará hincapié en la importancia de conceptos de ingeniería de software (componentes e interfaces entre componentes) para delinear la formalización inicialmente y como guías que permitan el desarrollo modular de la formalización. En este sentido, se espera que quien apruebe el curso comprenda la ventaja de definir tácticas (y el uso de meta-programación en general) para resolver tareas repetitivas.