Size: a a a

Compiler Development

2020 April 20

YR

Yurii Rashkovskii in Compiler Development
Но на прямо очень ранних, в основном какие-то аспекты обдумываю и обсуждаю. Интерес к этой теме в целом наблюдается в моей репрезентативной выборке
источник

DP

Dmitry Ponyatov in Compiler Development
Михаил Бахтерев
А где в этом теория категорий и прочие "ужасы"? Обычное ast
ну не знаю, на первый взгляд это больше похоже на формулу того, что нужно употребить чтобы понять самый примитивный учебник по Coq
источник

AG

Alex Gryzlov in Compiler Development
это просто двоичная система исчисления
источник

AG

Alex Gryzlov in Compiler Development
101 ={binary} 10 +{binary} 11
источник

AG

Alex Gryzlov in Compiler Development
только все максимально рассахарено
источник

IJ

Igor 🐱 Jirkov in Compiler Development
Dmitry Ponyatov
When dealing with integers, the user will enter the notation 5=2+3 but internally the Coq kernel
will be given the term:
@eq Z (Zpos (xI (xO xH))) (Zplus (Zpos (xO xH)) (Zpos (xI xH)))

да не спасибо
а что такое нормально же читается
источник

IJ

Igor 🐱 Jirkov in Compiler Development
даже числа у  вас в привычном бинарном формате даны
источник

DP

Dmitry Ponyatov in Compiler Development
а, RTL/HDL структурки тоже можно вертеть, прикольно
https://www.hindawi.com/journals/wcmc/2020/7346763/
источник

МБ

Михаил Бахтерев in Compiler Development
Dmitry Ponyatov
ну не знаю, на первый взгляд это больше похоже на формулу того, что нужно употребить чтобы понять самый примитивный учебник по Coq
Можно попробовать понять учебник по Lean. Он попроще и попонятнее. А потом уже перечитывать руководство по Coq.
источник

МБ

Михаил Бахтерев in Compiler Development
Интересно, но примеры жиденькие какие-то. Вроде, уже в 90-ых умели проверять на ACL2 32-битовые делители.
источник

AK

Andrei Kurosh in Compiler Development
K R
Там нужно как-то очень ловко совмещать сущности разной степени строгости.

С одной стороны, да, часто хочется объектов, без парсинга, без вылетов и с Хаскельной надёжностью. С другой стороны, интерактивная оболочка работает и в условиях, когда данные очень грязные - часто пишем какой-нибудь "grep тра-ля-ля xxx.log", а выхлопом являются как строки, которые нам нужны, так и шум, который мы отфильтровываем глазами - так быстрее, чем писать программу, выдающую те и только те данные, что нам нужны.

То есть, от интерпретатора командной строки требуется работа сразу на нескольких разных уровнях строгости - системные скрипты из /etc/init.d должны быть абсолютно надёжны, пользовательские - средне, интерактив - напиши и забудь. Наиболее близкое к этому, кажется gradual typing.
Так программа под nushell может возвращать структурированные данные и в то же время печатать произвольные данные в консоль в интерактивном режиме. Тот факт, что в классических шеллах эти потоки совмещены - просто исторически закрепившийся косяк архитектуры
источник

МБ

Михаил Бахтерев in Compiler Development
Andrei Kurosh
Так программа под nushell может возвращать структурированные данные и в то же время печатать произвольные данные в консоль в интерактивном режиме. Тот факт, что в классических шеллах эти потоки совмещены - просто исторически закрепившийся косяк архитектуры
И как печатать структурированные потоки данных? Можно ли на псевдокоде?

Потоки же закрепились, потому что с ними очень просто работать, и из них естественно вырастают сокеты и сети.

В принципе, были и более мощные реализации stream-ов, но они не прижились.
источник

AK

Andrei Kurosh in Compiler Development
Михаил Бахтерев
И как печатать структурированные потоки данных? Можно ли на псевдокоде?

Потоки же закрепились, потому что с ними очень просто работать, и из них естественно вырастают сокеты и сети.

В принципе, были и более мощные реализации stream-ов, но они не прижились.
Вот тут несколько наглядных и очень элегантных примеров:

https://www.nushell.sh/book/en/introduction.html
источник

МБ

Михаил Бахтерев in Compiler Development
Andrei Kurosh
Вот тут несколько наглядных и очень элегантных примеров:

https://www.nushell.sh/book/en/introduction.html
А куда перемотать, чтобы посмотреть, как программки на Си писать, чтобы выводить в nushell?
источник

AK

Andrei Kurosh in Compiler Development
Михаил Бахтерев
А куда перемотать, чтобы посмотреть, как программки на Си писать, чтобы выводить в nushell?
Честно говоря не знаю, но сейчас поищу. Я им активно не пользуюсь (как и консолью вообще), просто очарован элегантностью идеи. Сама консоль написана на Rust.
источник

МБ

Михаил Бахтерев in Compiler Development
Andrei Kurosh
Честно говоря не знаю, но сейчас поищу. Я им активно не пользуюсь (как и консолью вообще), просто очарован элегантностью идеи. Сама консоль написана на Rust.
Кажется, это самый важный аспект shell-строения. Ввод/вывод должен быть простым
источник

AK

Andrei Kurosh in Compiler Development
Михаил Бахтерев
Кажется, это самый важный аспект shell-строения. Ввод/вывод должен быть простым
Согласен. И это хорошо иллюстрирует мысль, с которой я начал вообще этот разговор про шеллы: даже очень перспективная идея, которая требует от людей отказаться от их привычной экосистемы (со всеми ее костылями и недостатками), обычно обречена быть уделом кучки энтузиастов
источник

МБ

Михаил Бахтерев in Compiler Development
Andrei Kurosh
Согласен. И это хорошо иллюстрирует мысль, с которой я начал вообще этот разговор про шеллы: даже очень перспективная идея, которая требует от людей отказаться от их привычной экосистемы (со всеми ее костылями и недостатками), обычно обречена быть уделом кучки энтузиастов
Новое не должно усложнять жизнь. Большинству программ богатый ввод/вывод не нужен. И если не нужно, он не должен усложнять жизнь. Как-то так это представляется. Если nushell нормально работает с потоками строк, то почему бы и нет?
источник

IJ

Igor 🐱 Jirkov in Compiler Development
Михаил Бахтерев
Новое не должно усложнять жизнь. Большинству программ богатый ввод/вывод не нужен. И если не нужно, он не должен усложнять жизнь. Как-то так это представляется. Если nushell нормально работает с потоками строк, то почему бы и нет?
Мне кажется,  в фантастических фильмах о будущем  многие примеры работы с футуристичными интерфейсами подразумевает поэтапный анализ данных, в который вовлечено очень много разных программных компонент
источник

IJ

Igor 🐱 Jirkov in Compiler Development
Это как раз может  подразумевать структурированный обмен данными между частями системы
источник