La semántica natural (coinductiva) se presenta como un marco unificador para la verificación de la corrección total de compiladores en Coq (con la característica de que se puede obtener un compilador verificado). De esta manera, tenemos un marco simple, fácil e intuitivo; para llevar a cabo la verificación de un compilador, utilizando un asistente de pruebas en el que se consideran ambos casos: computaciones terminantes y no terminantes (corrección total).