Володя - потусторонний шофёр
Интресное.

Then I was surrounded by a group of logisticians who trusted the connection
between type theories and set theory on faith and who tried to convince me
and others that mathematicians should do likewise.
It is only less than a year ago and due to the steadfast refusal of the
mathematical community to do so that I was able to disentangle myself from
them and to continue the work interrupted in 2009.

Прежде, чем объединяться, и для того, чтобы объединиться, мы должны сначала решительно и определенно размежеваться:

There is a theory that logicians developed that is based on concepts such as
meaning explanation or strong normalization that provides consistency proofs
for some sample type theories but it leads to the isolation of type theory from
the rest of mathematics rather than to their integration.

Если кто не верит в сильную нормализацию, это нам кафиры, короче.

На фото Владимир Воеводский переосмысливает теории Мартин-Лефа с точки зрения современной математики: