Здравствуйте, kochetkov.vladimir, Вы писали:
M>>- как доказывать правильность этих DSL'ей? KV>А можешь развить мысль поподробнее? Что ты вкладываешь в понятние "правильности" DSL и каковы критерии доказнности этой правильности?
Думаю речь о написание непротиворечивого языка. Тут вот постоянно приводят разные примеры, типа регулярных выражений и т.п... А вот если бы тебе надо было придумать свой язык типа них (при этом ты никогда раньше не видел других вариантов), то за какое время ты бы справился? ) Причём речь даже не о конкретном наборе метасимволов, классов, групп, квантификаторов, а о самих этих понятиях. Это ведь ты сейчас уже с ними знаком, а автору подобного языка надо в начале ввести эти понятия, и только потом наполнить их смыслом с помощью конкретной реализации. На мой взгляд это не такая уж тривиальная задачка для рядового кодера...
Ну и да, вопрос насчёт формальной проверки правильности конечно не совсем корректен. Мне кажется, что такие вещи проверяются скорее практикой (причём годами). Но в том то и вопрос, если мы говорим о повсеместном использование DSL'ей.
P.S. Если что, я сам частенько использую DSL'и, но в основном имеющие какой древний фундаментальный языковой базис. Т.е. обычно речь идёт о нестандартной реализации (типа edsl в C++ например) давно известного синтаксиса.
M>>- как доказывать правильность этих DSL'ей?
KV>А можешь развить мысль поподробнее? Что ты вкладываешь в понятние "правильности" DSL и каковы критерии доказнности этой правильности?
но добавлю еще одно. Это безапеляционные (и постоянные, нескончаемые) потоки пафосных заявлений о том, что <X из Немерле> генерирует правильный код, быстродейственный код и т.п., который вручную ну никак не написать, ибо.
Любая просьба доказать это разбивается о «верь мне это так, потому что мы д'Артаньяны».
В любом новом языке есть два уровня. Первое: правильность реализации самого языка. Второе: правильность реализованных на нем программ. Как это достигается на DSL'ях? А никому неизвестно
Здравствуйте, alex_public, Вы писали:
_>Думаю речь о написание непротиворечивого языка.
А непротиворечивый формальный язык — это ... ? =/
_>Тут вот постоянно приводят разные примеры, типа регулярных выражений и т.п... А вот если бы тебе надо было придумать свой язык типа них (при этом ты никогда раньше не видел других вариантов), то за какое время ты бы справился? ) Причём речь даже не о конкретном наборе метасимволов, классов, групп, квантификаторов, а о самих этих понятиях. Это ведь ты сейчас уже с ними знаком, а автору подобного языка надо в начале ввести эти понятия, и только потом наполнить их смыслом с помощью конкретной реализации. На мой взгляд это не такая уж тривиальная задачка для рядового кодера...
Довод понятен, ок. Только реглуярные выражения здесь не очень удачный пример, т.к. современную форму они приобрели эволюционным путем, а изначально были сформулированы для несколько иной задачи — компактного языка для описания конечных автоматов. Ну и задачи разработки DSL и самой предметной области стоит все же разделять. Проектирование и формализация предметной области — задача вообще не для кодера.
Здравствуйте, Mamut, Вы писали:
M>>>- как доказывать правильность этих DSL'ей?
KV>>А можешь развить мысль поподробнее? Что ты вкладываешь в понятние "правильности" DSL и каковы критерии доказнности этой правильности?
M>Ну, alex_public уже в целом написал тут
Он написал правильные вещи, с которыми я в целом согласен, но ответа на мой вопрос там нет
M>но добавлю еще одно. Это безапеляционные (и постоянные, нескончаемые) потоки пафосных заявлений о том, что <X из Немерле> генерирует правильный код, быстродейственный код и т.п., который вручную ну никак не написать, ибо. M>Любая просьба доказать это разбивается о «верь мне это так, потому что мы д'Артаньяны».
Не-не-не. Жаловаться на гадких немерлистов мне не надо — люди взрослые, сами разберетесь. Я задал конкретный вопрос, желая дать вполне конкретный ответ на твой. Безотносительно идущего спора о Nemerle, ок?
M>В любом новом языке есть два уровня. Первое: правильность реализации самого языка.
Вот я об этом. Что является формальным критерием правильности реализации самого языка?
M>Второе: правильность реализованных на нем программ. Как это достигается на DSL'ях? А никому неизвестно
Я даже больше скажу. Если ты поинтересуешься, как это достигается на тьюринг-полных языках, то узнаешь, что там это является алгоритмически-неразрешимой задачей. Откуда взялось утверждение, что для DSL эта задача должна быть разрешима?
Здравствуйте, kochetkov.vladimir, Вы писали:
KV>Довод понятен, ок. Только реглуярные выражения здесь не очень удачный пример, т.к. современную форму они приобрели эволюционным путем, а изначально были сформулированы для несколько иной задачи — компактного языка для описания конечных автоматов.
Интересно, а какие-то распространённые современные конструкции получились не эволюционным путём? )
KV>Ну и задачи разработки DSL и самой предметной области стоит все же разделять. Проектирование и формализация предметной области — задача вообще не для кодера.
Ну так тогда надо понимать, кто конкретно является целевой аудиторией для инструмента, помогающего проектировать DSL'и. И каков вообще её размер (очевидно намного меньше просто программистской, даже если забыть о фрагментации на языки, платформы и т.п.).
Здравствуйте, kochetkov.vladimir, Вы писали:
KV>Я даже больше скажу. Если ты поинтересуешься, как это достигается на тьюринг-полных языках, то узнаешь, что там это является алгоритмически-неразрешимой задачей. Откуда взялось утверждение, что для DSL эта задача должна быть разрешима?
Все дело в модели. Любой язык всего лишь описывает ту или иную модель. Всегда можно создать простую модель, которую не сложно проверить. DSL-и обычно подразумевают существенно более простые модели нежели ЯП общего назначения (ЯПОН).
Языковый подход отличается от подхода где модели описываются на некотором ЯПОН тем, что при применении языкового подхода есть стадия проверки ограничений. Это не означает, что эти проверки абсолютно корректны и полны, но это позволяет поймать ошибки и сообщить о них пользователю. Естественно, что если модель, лежащая под языком некорректная, то никакие проверки не помогут. Но в отличии от моделей описываемых на ЯПОН об ошибках можно знать заранее и получать намного более полную информацию, а не рантайм-вылеты с невнятной диагностикой.
На практике любой язык отлаживается как и любая другая программа. Если по DSL генерируется некий код на ЯПОН, то могут случаться так называемые протечки абстракции, т.е. не отловленные во время проверок ошибки вызывают генерацию некорректного кода на который ругается ЯПОН. Другой вариант протечки абстракции — рантам ошибки, которые могло бы не быть (как и в моделях на основе ЯПОН).
Есть логика намерений и логика обстоятельств, последняя всегда сильнее.
Здравствуйте, kochetkov.vladimir, Вы писали:
KV>Здравствуйте, Mamut, Вы писали:
M>>- как доказывать правильность этих DSL'ей?
KV>А можешь развить мысль поподробнее? Что ты вкладываешь в понятние "правильности" DSL и каковы критерии доказнности этой правильности?
На практике единственное, что требуют от DSL/modeling тулов с кодогенерацией, так это чтоб по одной и той же модели (или DSL) ВСЕГДА генерился один и то же код. По возможности, лучше чтоб time stamp-ы (modification date) на файлах не менялись если контент их не меняется при перегенрации.
Такое требование получали от telecom/military кастомеров, кто активно юзает кодогенерацию в продакшене.
