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

групп:

каналов:

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

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

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

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

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

go.backupland.com

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

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

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

Size: a a a

Compiler Development

816 membersпожаловаться на группу
2020 March 16

К

Константин in Compiler Development
Peter Sovietov
Что-то уж очень притянуто за уши. Согласитесь, мало смысла компиляторщику рассуждать о формальных методах, если он не понимает, как их применить в своей области.
А чем формально записанный синтаксис - это не формальный метод? Или Вы только о доказательствах?
источник
15:29пожаловаться#1

AT

Anton Trunov in Compiler Development
MaxGraey
Инетерестно кстати кто какрешает парадоксы теории множеств в формальных методах
используют теории множеств без парадоксов)
источник
15:30пожаловаться#2

К

Константин in Compiler Development
Михаил Бахтерев
Лично мой вопрос об архитектуре компилятора. Можно делать так, чтобы теория типов была опциональной, допустим так, как сделано с LaTTe в Clojure. А можно её enforce-ить в языке. Что  лучше. Не могу решить без внешних мнений.
Опционально, разумеется
источник
15:30пожаловаться#3

EM

Evgenii Moiseenko in Compiler Development
MaxGraey
Инетерестно кстати кто какрешает парадоксы теории множеств в формальных методах
Вся теория типов выросла из попыток решить парадокс Расселла :)
источник
15:31пожаловаться#4

PS

Peter Sovietov in Compiler Development
Константин
А чем формально записанный синтаксис - это не формальный метод? Или Вы только о доказательствах?
Вот это уже конкретика. Да, БНФ  — это самая настоящая формальная спецификация. В ее коде, безусловно, можно совершить ошибки, она может быть исполняемой, можно доказать корректность трансляции из БНФ в целевой код.
источник
15:31пожаловаться#5

M

MaxGraey in Compiler Development
Anton Trunov
используют теории множеств без парадоксов)
Ну этосильно зависит от нотации, вот та же Z-нотация подобрана таким образом, что бы избегать, да
источник
15:32пожаловаться#6

К

Константин in Compiler Development
Михаил Бахтерев
Лично мой вопрос об архитектуре компилятора. Можно делать так, чтобы теория типов была опциональной, допустим так, как сделано с LaTTe в Clojure. А можно её enforce-ить в языке. Что  лучше. Не могу решить без внешних мнений.
нужна возможность для плавного перехода. И что за компилятор?
источник
15:32пожаловаться#7

AT

Anton Trunov in Compiler Development
MaxGraey
Ну этосильно зависит от нотации, вот та же Z-нотация подобрана таким образом, что бы избегать, да
я имею в виду, никто не использует наивную теорию множеств для пруверов
источник
15:32пожаловаться#8

К

Константин in Compiler Development
Peter Sovietov
Вот это уже конкретика. Да, БНФ  — это самая настоящая формальная спецификация. В ее коде, безусловно, можно совершить ошибки, она может быть исполняемой, можно доказать корректность трансляции из БНФ в целевой код.
И сколько преимуществ даёт для всех - для разработчиков языка, разработчиков компилятора, пользователя языка
источник
15:33пожаловаться#9

МБ

Михаил Бахтерев in Compiler Development
Peter Sovietov
Вот это уже конкретика. Да, БНФ  — это самая настоящая формальная спецификация. В ее коде, безусловно, можно совершить ошибки, она может быть исполняемой, можно доказать корректность трансляции из БНФ в целевой код.
Имеются в виду формальные доказательства? А есть примеры?
источник
15:34пожаловаться#10

МБ

Михаил Бахтерев in Compiler Development
Ну, кроме Compcert, конечно
источник
15:34пожаловаться#11

К

Константин in Compiler Development
А в нём, как раз этого не было
источник
15:34пожаловаться#12

К

Константин in Compiler Development
там генерация
источник
15:34пожаловаться#13

PS

Peter Sovietov in Compiler Development
Anton Trunov
я имею в виду, никто не использует наивную теорию множеств для пруверов
С точки зрения практика мы просто кванторы переводим в режим compile-time, соответственно речь уже идет о конечных множествах :)
источник
15:35пожаловаться#14

AT

Anton Trunov in Compiler Development
MaxGraey
Ну этосильно зависит от нотации, вот та же Z-нотация подобрана таким образом, что бы избегать, да
вообще в этой области скорее проблема не в парадоксах, а в том, что некоторые формальные системы не дают возможности эффективно моделировать, т.к. сильно размер артефактов растет
источник
15:35пожаловаться#15

PS

Peter Sovietov in Compiler Development
Константин
И сколько преимуществ даёт для всех - для разработчиков языка, разработчиков компилятора, пользователя языка
Вот. А еще есть язык спецификаций для статической семантики, для динамической семантики, для трансформаций программ... А мы все с subtract возимся! :)
источник
15:36пожаловаться#16

AT

Alexander Tchitchigin in Compiler Development
Михаил Бахтерев
Лично мой вопрос об архитектуре компилятора. Можно делать так, чтобы теория типов была опциональной, допустим так, как сделано с LaTTe в Clojure. А можно её enforce-ить в языке. Что  лучше. Не могу решить без внешних мнений.
POPL 2016: Takikawa, Feltey, Greenman, New, Vitek, and Felleisen
Is sound gradual typing dead?
http://www.ccis.neu.edu/racket/pubs/popl16-tfgnvf.pdf
источник
15:36пожаловаться#17

МБ

Михаил Бахтерев in Compiler Development
Alexander Tchitchigin
POPL 2016: Takikawa, Feltey, Greenman, New, Vitek, and Felleisen
Is sound gradual typing dead?
http://www.ccis.neu.edu/racket/pubs/popl16-tfgnvf.pdf
Ага. Я читал.
источник
15:37пожаловаться#18

AT

Alexander Tchitchigin in Compiler Development
Михаил Бахтерев
Ага. Я читал.
Выводы довольно печальны, как по мне. 😞
источник
15:37пожаловаться#19

МБ

Михаил Бахтерев in Compiler Development
Alexander Tchitchigin
Выводы довольно печальны, как по мне. 😞
Ну, да... Ужа с ежом плохо получается скрещивать. Typed Racket вот довольно... Ну. Костыльный местами. Но я себе мыслю нечто типа такого. Есть базовый динамический язык, и мы не делаем его типизированным, но в некотором DSL можем доказывать свойства отдельных функций.
источник
15:40пожаловаться#20