Код на Sound, который вы написали, потом транслируется в код на си? Если да, то как вызывать получившуюся функцию из другого кода на си так, чтобы формальная спецификация имела смысл? Вот мы получили calc_sum, которая соответствует формальной спецификация, а потом где-то ошиблись в вызове:
int arr[12] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11};
// Тут произойдёт выход за границу массива
int result = calc_sum(arr, 15);
Честно говоря, ничего из написанного не понял. Чем Sound отличается от любого существующего средства проверки теорем типа Coq или Agda, на которых можно формально доказывать корректность кода?
Технология Sound может быть реализована в рамках любого языка программирования, поэтому язык Sound можно транслировать в любой ЯП
Что вообще значит это предложение? Sound - это язык или технология? Если язык, то возможность реализации компилятора Sound на языке X не доказывает возможность трасляции Sound в язык X. Если технология, то вообще не понятно, что такое Sound и как его траслировать.
В единственном приведённом примере кода не понятно, где собственно формальная верификация.
На примере Rust по идее не вышло бы про типы-объединения рассказать, так как в нём они не поддерживаются, потому что Rust компилируемый язык, а при компиляции всегда нужно знать, какой тип у переменной. То есть если в интерпретируемых языках я могу сделать проверку вида: typeof(var) == "int", то в компилируемых языках для этого придётся использовать теги, что собственно в типах-суммах и делается.
Вопрос 1: Как трансляция в интерпретируемый язык программирования, зависимый от js, связана с компиляцией?
Скажу в защиту автора, что это зависит от определения компиляции. В драконьей книге было дано следующее определение (не дословная цитата): "Компиляция - это перевод программы с одного языка на другой с сохранением семантики"
Назначение и применение данного проекта не подлежат сомнению – он служит настоящим мощным инструментом для создания трансляторов, интерпретаторов и компиляторов. Если вы хотите разработать свой собственный язык программирования или преобразовать имеющийся язык в компилируемый формат, то этот проект, безусловно, является вашим незаменимым союзником.
Что мне мешает использовать для этих целей настоящий LLVM? Он, в отличие от вашего самозванца, выдаёт оптимизированный нативный код, а не код на интерпретируемом языке. И сразу возникает вопрос, что же такое "компилируемый формат"? Зачем вы собственные никому не понятные термины придумываете?
Codegen же отвечает за создание машинного кода и обеспечивает оптимизацию, что повышает эффективность программы.
Зачем врать? Asmx - не машинный код.
Давайте напишем грамматику для создания переменной или константы. В файле grammar.json добавляем следующий код:
То есть форматы идентификаторов, чисел и строк вы выбрали сами за разработчика компилятора и он никак не может их поменять. А где же обещанная гибкость? Ещё возникает вопрос, а могу ли описать с помощью данной грамматики выражение, в котором у операций есть приоритеты, например, простейший случай:
<expr> ::= <term>
| <expr> + <term>
| <expr> - <term>
<term> ::= <fact>
| <term> * <fact>
| <term> / <fact>
<fact> ::= <var>
| (<expr>)
<var> ::= A | B | C ... | X | Y | Z
Это язык, в котором переменная задаётся одной латинской буквой, есть сложение, вычитание, умножение и деление, причём последние две операции имеют приоритет. Покажите пример грамматики для llvm.js, которая разбирает данный язык.
Проект llvm.js стоит применять всем разработчикам, стремящимся сэкономить время и ресурсы при создании собственных языков программирования или превращении существующих языков в компилируемые. Благодаря этому инновационному инструменту, вы сможете добиться впечатляющих результатов в кратчайшие сроки и привнести новую эру в мир программирования.
Не понятно зачем? Можно взять почти для любого языка flex и bison или их аналоги и сделать лексер и парсер довольно быстро, а плюсом получить гибкость, которой вы лишили разработчика. Для быстрой разработки можно взять haskell или ocaml, так как на них намного легче разрабатывать компиляторы и интерпретаторы, и использовать биндинги к настоящему llvm.
Выводы, конечно, поражают.
В завершение статьи мы провели простую компиляцию JavaScript кода с использованием llvm.js. Мы создали компилятор и успешно скомпилировали JavaScript код в AsmX. Этот пример продемонстрировал мощь и гибкость llvm.js и его способность к работе с разными языками программирования.
Где компилятор JavaScript? В статье был сделан "компилятор" языка, в котором можно присваивать переменным значения и выводить их в консоль, всё.
В целом, llvm.js представляет собой мощное средство для разработчиков, которые работают в области создания языков программирования и интерпретаторов/компиляторов. Он предоставляет широкий набор компонентов и функций, которые значительно упрощают процесс создания новых языков и обеспечивают быстрое развертывание и выполнение кода на различных языках. И хотя llvm.js не связан непосредственно с LLVM, они оба основаны на тех же принципах и позволяют разработчикам использовать их мощь для создания эффективных и производительных приложений.
По всем пунктам нет. Нативный код быстрее, чем интерпретируемый на Asmx. llvm.js не является мощным и гибким средством.
Вы сделали неплохой хобби проект, но совершенно нигде не применимый. А описали его так, будто бы революцию по меньшей мере совершили.
Дело ваше, но можно сразу перейти к продвинутому освещению и теням, зачем описать то, что уже было на русском языке описано множество раз? Ну и вместо функционального псевдоязыка, можно использовать настоящий, например haskell. Под него есть библиотеки https://hackage.haskell.org/package/massiv и https://hackage.haskell.org/package/repa, которые позволяет легко писать параллельные вычисления для массивов, что в общем-то и требуется для трассировки лучей.
А в чём смысл очередной статьи про трассировку лучей? На хабре их уже было много, лучшая, как по мне эта https://habr.com/ru/articles/436790. Не хватает статей, которые идут дальше рисования сферы/куба/конуса/etc, а именно статей, где бы подробнее рассматривалось освещение, тени и материалы, потому что картинка, которая получается в результате среднестатистического трассировщика из статьи выглядит совершенно нереалистично и некрасиво.
А как тогда отладкой заниматься? Процессу, запущенному с правами администратора должно быть можно всё. Если процесс пользовательский, то по умолчанию разрешить ему отлаживать только дочерние процессы. Плюсом можно дать возможность запрещать пользовательским процессам отладку вовсе
В том, что при разрыве соединения скрипт исполнится не полностью, а также в том, что можно распознать curl или wget, который передаёт данные в bash, и возвращать что-нибудь нехорошее
Автор, пишите ещё. Ваша работа со словом - это нечто уникальное, давно я не получал такого удовольствия от чтения.
AsmX - это кроссплатформенный язык программирования с полной поддержкой Тьюринга.
AsmX предлагает ряд возможностей, таких как корутины, которые могут быть легко манипулированы.
Минусаторы, где вы ещё найдёте полную поддержку Тьюринга и легко манипулируемых корутин?
А если серьёзно, я требую добавить в следующую версию AsmX полную поддержку Алонзо Чёрча, тогда мы все проекты в проде переведём на AsmX и будем в него контрибьютить.
Я совсем не фата раста, т.к. мне на нём сложно писать, но профит от его использования хотя бы понятен - он не позволяет тебе делать многие небезопасные вещи, в т.ч. позволяет безопасно работать с памятью без GC. А в чём крутость питона с типами (если я правильно понял суть Mojo), это же просто очередной язык с GC
Код на Sound, который вы написали, потом транслируется в код на си? Если да, то как вызывать получившуюся функцию из другого кода на си так, чтобы формальная спецификация имела смысл? Вот мы получили calc_sum, которая соответствует формальной спецификация, а потом где-то ошиблись в вызове:
Если нет, что с ним после написания делать?
Понятнее не стало. Вот, например, есть программа на си, вычисляющая сумму массива. Как мне в неё спецификацию на Sound ввести?
Честно говоря, ничего из написанного не понял. Чем Sound отличается от любого существующего средства проверки теорем типа Coq или Agda, на которых можно формально доказывать корректность кода?
Что вообще значит это предложение? Sound - это язык или технология? Если язык, то возможность реализации компилятора Sound на языке X не доказывает возможность трасляции Sound в язык X. Если технология, то вообще не понятно, что такое Sound и как его траслировать.
В единственном приведённом примере кода не понятно, где собственно формальная верификация.
Мне статья понравилась, правда в развлекательном плане, а не техническом. Её бы в хаб юмор переместить, и все довольны остануться.
Я с крестами не особо знаком, но разве typeid не во время компиляции вычисляется?
UPD:
Если брать union в c++, то там нет возможности определить какой член является установленным, насколько я знаю:
В си такого нету. Есть typeof, но он работает только потому что компилятор знает тип переменной. Что-то вроде такого:
int var = 123;typeof(var) y = 345;Нормального примера использования typeof сходу не вспомнил.
На примере Rust по идее не вышло бы про типы-объединения рассказать, так как в нём они не поддерживаются, потому что Rust компилируемый язык, а при компиляции всегда нужно знать, какой тип у переменной. То есть если в интерпретируемых языках я могу сделать проверку вида:
typeof(var) == "int", то в компилируемых языках для этого придётся использовать теги, что собственно в типах-суммах и делается.Судя по статье по ссылке, Union Types - это и есть сумма типов, просто в TS нужно через typeof тип проверять, а не через pattern matching
Скажу в защиту автора, что это зависит от определения компиляции. В драконьей книге было дано следующее определение (не дословная цитата): "Компиляция - это перевод программы с одного языка на другой с сохранением семантики"
Что мне мешает использовать для этих целей настоящий LLVM? Он, в отличие от вашего самозванца, выдаёт оптимизированный нативный код, а не код на интерпретируемом языке. И сразу возникает вопрос, что же такое "компилируемый формат"? Зачем вы собственные никому не понятные термины придумываете?
Зачем врать? Asmx - не машинный код.
То есть форматы идентификаторов, чисел и строк вы выбрали сами за разработчика компилятора и он никак не может их поменять. А где же обещанная гибкость? Ещё возникает вопрос, а могу ли описать с помощью данной грамматики выражение, в котором у операций есть приоритеты, например, простейший случай:
Это язык, в котором переменная задаётся одной латинской буквой, есть сложение, вычитание, умножение и деление, причём последние две операции имеют приоритет. Покажите пример грамматики для llvm.js, которая разбирает данный язык.
Не понятно зачем? Можно взять почти для любого языка flex и bison или их аналоги и сделать лексер и парсер довольно быстро, а плюсом получить гибкость, которой вы лишили разработчика. Для быстрой разработки можно взять haskell или ocaml, так как на них намного легче разрабатывать компиляторы и интерпретаторы, и использовать биндинги к настоящему llvm.
Выводы, конечно, поражают.
Где компилятор JavaScript? В статье был сделан "компилятор" языка, в котором можно присваивать переменным значения и выводить их в консоль, всё.
По всем пунктам нет. Нативный код быстрее, чем интерпретируемый на Asmx. llvm.js не является мощным и гибким средством.
Вы сделали неплохой хобби проект, но совершенно нигде не применимый. А описали его так, будто бы революцию по меньшей мере совершили.
Перевод машинный?
Получается, что компилятор на локальной машине уже компилятором не является.
Дело ваше, но можно сразу перейти к продвинутому освещению и теням, зачем описать то, что уже было на русском языке описано множество раз? Ну и вместо функционального псевдоязыка, можно использовать настоящий, например haskell. Под него есть библиотеки https://hackage.haskell.org/package/massiv и https://hackage.haskell.org/package/repa, которые позволяет легко писать параллельные вычисления для массивов, что в общем-то и требуется для трассировки лучей.
А в чём смысл очередной статьи про трассировку лучей? На хабре их уже было много, лучшая, как по мне эта https://habr.com/ru/articles/436790. Не хватает статей, которые идут дальше рисования сферы/куба/конуса/etc, а именно статей, где бы подробнее рассматривалось освещение, тени и материалы, потому что картинка, которая получается в результате среднестатистического трассировщика из статьи выглядит совершенно нереалистично и некрасиво.
А как тогда отладкой заниматься? Процессу, запущенному с правами администратора должно быть можно всё. Если процесс пользовательский, то по умолчанию разрешить ему отлаживать только дочерние процессы. Плюсом можно дать возможность запрещать пользовательским процессам отладку вовсе
https://lukespademan.com/blog/the-dangers-of-curlbash/
В том, что при разрыве соединения скрипт исполнится не полностью, а также в том, что можно распознать curl или wget, который передаёт данные в bash, и возвращать что-нибудь нехорошее
Автор уже изменил текст на "имеет полный Тьюринг". Боюсь спросить, что же там такого с Тьюрингом делают
Автор, пишите ещё. Ваша работа со словом - это нечто уникальное, давно я не получал такого удовольствия от чтения.
Минусаторы, где вы ещё найдёте полную поддержку Тьюринга и легко манипулируемых корутин?
А если серьёзно, я требую добавить в следующую версию AsmX полную поддержку Алонзо Чёрча, тогда мы все проекты в проде переведём на AsmX и будем в него контрибьютить.
Только в си нет интерфейсов
Насколько я понял, оно будет опциональным, что не позволяет убрать GC. Вот пример с официального сайта:
Поэтому особого смысла в его использовании я не вижу.
Я совсем не фата раста, т.к. мне на нём сложно писать, но профит от его использования хотя бы понятен - он не позволяет тебе делать многие небезопасные вещи, в т.ч. позволяет безопасно работать с памятью без GC. А в чём крутость питона с типами (если я правильно понял суть Mojo), это же просто очередной язык с GC