KR
ну трейд-оффы везде есть, да. но если верить автору идрис, то большинство доказательств в коде тривиальны по сравнению с матаном
по факту заканчивается джунами JS'никами с пустым взглядом в монитор)
Ну так себе, с исторической перспективы это важно.
Как раз в какой-то момент большинство, если не все, языки с гц были без вм