(
о кстати
> скучно
Это уже совсем другое дело же.
Size: a a a
2021 May 27
(
а погнали верифицированную ось на идрисе напишем
IP
Я бы arend предпочел, но его еще подучить немного надо
IP
И в HoTT вкатиться
(
аренд во что-то полезное не заэкстрактишь, плюс хотт для такой задачи оверкилл
(
он же нужен для прувов, которые требуют функциональной экстенсиональности
IP
Ну типа. А вдруг я в вуз поступлю
AM
Мне кажется, или ОС целиком верифицированной делать долго и бессмысленно?
(
ос нынче в целом делать бессмысленно
IP
Там на третьем семестре заботаю какой-нибудь набор инструкций.
IP
AM
Аргумент
(
хотя я бы запилил самую лучшую ось для мобильных устройств
(
без всей этой ебли с андроид сдк
AD
Смысленно
AD
В наса пытаются
AG
Ну и фуксию зачем-то написали.