Без заголовка

На тех уровнях абстракции, о которых мы говорим, нельзя говорить о "машинном языке" (хотя можно перейти на язык "исполнителей" и "выполнителей" -- правда, с осторожностью. Ибо в оригинале эти термины были введены для императивных языков, а у нас совсем не факт, что что-то "выполняется". Может и "оцениваться", например). Если оценка формализована, то это сводимо к выполняется на специфичной абстрактной машине. К примеру, в Coq, доказательство теоремы, сводится к конструированию функции, которая потом "оценивается" системой: система вычисляет ее тип, ну и проверяет, что он сводим к целевому типу (то что нужно доказать, формулируется в виде типа). Поскольку proof-term редко конструируют вручную, то программер пишет всякие конструкции/программы, которые вычисляют доказательство (транслируются в него), а потом система оценивает, что получилось то что нужно.