АП
Переслано от Антон Пилипчук...
Size: a a a
2021 July 07
ДК
А вы разобрались? Я смотрю, и вижу фигу: куча спецзначков и никаких комментариев. Куда там смотреть, чтобы увидеть, что именно верифицировано?
[
всё верифицировано
AG
в статью надо смотреть
ДК
Что всё?
[
весь мир
AG
вот здесь как я понимаю центральное док-во https://github.com/sergei-romanenko/agda-simple-scp/blob/master/LoopUnrollingScp.agda#L143-L146
ДК
@clayrat Спасибо!
AG
учтите только что статья на coq, а в репе порт на агду
ДК
На Coq всё гораздо понятнее. Мда...
AG
злоупотребление юникодом это классическая претензия к агдистам да :)
AG
но там есть и более тонкие отличия
AG
недавно в одном из чатов проскакивала мысль, что нетипизированные языки кажутся новичкам проще, т.к. не надо держать в голове отдельно семантику тайпчекера и рантайма, достаточно последней
AG
вот агда это что-то похожее в плане того, что она прячет разницу между метаязыком и низкоуровневым "ассемблером" доказательств
[
Если мы берём какие-то шарпы, то там этого тайпчекера на пол часа изучения
[
К тому же в питоне и жс тоже надо учить как работают типы
[
Отсутствие типов не выливается в отсутствие необходимости тайпчека
[
Просто его должен делать кодер руками
AG
ключевая фраза "кажутся новичкам проще"