В рейтинге участвует:

групп:

каналов:

Виртуальный сервер на SSD - недорого!

Аренда выделенных и виртуальных серверов (VDS/VPS), хостинг, аренда IP-адресов, администрирование, круглосуточная поддержка

qwarta.ru подробнее

Резервное копирование с проверкой на вирусы!!!

Удобный сервис создания резервных копий на любой сервер сети интернет. Отслеживайте изменения, проверяйте на вирусы. Надежно защитите свой бизнес!

go.backupland.com

Выбираете сервер? Любая конфигурация на заказ!

Аренда физических серверов любых конфигураций под любые запросы - 1С бухгалтерия, игровые сервера, нагруженные проекты, интернет-магазины!

qwarta.ru подробнее

Size: a a a

Compiler Development

1014 membersпожаловаться на группу
2021 April 27

МБ

Михаил Бахтерев... in Compiler Development
minlog тоже, потому что основана на реализуемости. ACL2 тоже, потому что это аппликативный фрагмент Лиспа. Но, всё равно, не особо и взлетело. Хотя, вроде как, ACL2 используют в индустрии.

Почему это важно для компиляторов? Потому что у нас есть другие логики, которые можно использовать во всяких разных доказательствах свойств на разных стадиях оптимизации кода.
источник
21:45пожаловаться#1

МБ

Михаил Бахтерев... in Compiler Development
Но вот, кстати, у minlog даже может быть преимущество именно для описания вычислительных процедур, потому что это параконсистентная логика, которая не боится рекурсивностей и брадобреев.
источник
21:49пожаловаться#2

AT

Alexander Tchitchigi... in Compiler Development
Я тут смотрел простенькие доказательства на ACL2 -- очень трудно разобраться. И это как раз из-за автоматизации и "заметания под ковёр" пруф-термов. Оказывается, на практике это не так здорово, как кажется. Многим и доказательства тактиками не нравятся, а тут вообще без "опорного конспекта".
источник
21:51пожаловаться#3

МБ

Михаил Бахтерев... in Compiler Development
Ну, в ACL2 и нет proof-термов в обычном понимании. Там есть целевой терм, к которой идут эвристики, и которым надо подсказывать, как идти. Вот кстати, очень похоже на то, что делают оптимизаторы.
источник
21:59пожаловаться#4

KR

K R in Compiler Development
Спасибо. Подтверждает моё наблюдение, что внутри каждого программиста есть свой QC. И количество ошибок в результирующем коде зависит от этого QC.

Соответственно по языкам надо мерить не кол-во ошибок, а время написания с отладкой типичного для предметной области кода на разных языках.
источник
22:01пожаловаться#5

KR

K R in Compiler Development
Там, конечно, будет нелинейная зависимость от объёма.
источник
22:01пожаловаться#6

AT

Alexander Tchitchigi... in Compiler Development
Вот на практике это создаёт проблемы, так ACL2 и не пользуется оглушительной популярностью.

Кроме того, композициональность получается "интересная": при наличии лемм, теорема доказывается, а без них -- нет. Хотя леммы сами по себе доказываются автоматически, то есть ACL2 как бы может вывести всё, что нужно. Но не вместе, а только частями. Размер которых заранее совершенно не понятен.
источник
22:06пожаловаться#7

МБ

Михаил Бахтерев... in Compiler Development
Почему внутренние? Есть всякие тесты, spec-и, fuzzing и т.д. и т.п. Ну, то есть, есть технологии для самых разных языков, которые позволяют повышать качество тем или иным способом. Сложные типы -- одна из технологий. А время и объёмы -- очень индивидуально. Вроде как, пытались такие исследования проводить, но они ничего особого не показывают, кроме того, что есть хорошие и плохие программисты.
источник
22:07пожаловаться#8

KR

K R in Compiler Development
На внешние всегда можно забить. Творческий труд отличается тем, что его часто проще переделать, чем проконтролировать.

Как показывает практика кровавого ынтырпрайза, всё обходится при желании - и типы, и тесты, и рецензии.
источник
22:08пожаловаться#9

МБ

Михаил Бахтерев... in Compiler Development
Зависит от рабочего процесса. Типы, всё равно, не решают всех проблем и тестировать необходимо. Хотя бы по той причине, что сами спецификации могут содержать ошибки. Примеров уйма. Я не отрицаю пользу типов, но одними типами не обойтись.
источник
22:20пожаловаться#10

DF

Dollar Føølish in Compiler Development
Хорошие и плохие программисты ... Кому из них больше нужны типы а кому тесты ?
источник
22:24пожаловаться#11

А

Алексей ayaye :)... in Compiler Development
парное программирование, один хороший, другой плохой
источник
22:28пожаловаться#12

DF

Dollar Føølish in Compiler Development
Один с тестами другой с типами
источник
22:29пожаловаться#13

МБ

Михаил Бахтерев... in Compiler Development
Тесты нужны всем.
источник
22:29пожаловаться#14
2021 April 28

B

Brenoritvrezorkre in Compiler Development
Параконсистентность не про рекурсивность...
источник
00:02пожаловаться#15

B

Brenoritvrezorkre in Compiler Development
Есть определённые исследования того, как бы описать самореферентный язык, в тусовке параконсистентных логиков, но параконсистентность — это просто отсутствие принципа взрыва (и желательно также взрыва негаций), который никак не связан ни с семантическими парадоксами, ни с парадоксами [наивной] теории множеств.
источник
00:07пожаловаться#16

B

Brenoritvrezorkre in Compiler Development
Принцип взрыва — это то, что из противоречия следует любое утверждение
источник
00:10пожаловаться#17

B

Brenoritvrezorkre in Compiler Development
Интуиционистская логика, например, его содержит
источник
00:11пожаловаться#18

B

Brenoritvrezorkre in Compiler Development
А минимальная уже нет
источник
00:11пожаловаться#19

B

Brenoritvrezorkre in Compiler Development
Но минимальная содержит то, что любая негация следует из противоречия
источник
00:11пожаловаться#20