Программирование в форме диалога. Часть I. Зачем это нужно
Программирование в форме диалога. Часть II. Реализация диалога, предыстория
Программирование в форме диалога. Часть III. Реализация диалога, будущее

Переход к написанию программы компьютером — это переход от монолога, к диалогу. При этом, так же как и при диалоге человека с человеком, у компьютера должна быть своя, внутренняя модель программы. У компьютера должна быть возможность вводить новые понятия (в терминах которых эта модель и будет выражена). Он будет общаться с человеком (программистом) на некотором языке (языках), достаточно независимом от внутренней модели программы. Эта модель будет изменяться не непосредственно программистом, а в результате диалога между компьютером и программистом. Эти языки общения будут специально приспособлены для удобства понимания человеком и его команд, а модель программы внутри компьютера будет приспособлена для работы с ней компьютером, а не человеком.

M>

M>Переход к написанию программы компьютером — это переход от монолога, к диалогу. При этом, так же как и при диалоге человека с человеком, у компьютера должна быть своя, внутренняя модель программы. У компьютера должна быть возможность вводить новые понятия (в терминах которых эта модель и будет выражена). Он будет общаться с человеком (программистом) на некотором языке (языках), достаточно независимом от внутренней модели программы. Эта модель будет изменяться не непосредственно программистом, а в результате диалога между компьютером и программистом. Эти языки общения будут специально приспособлены для удобства понимания человеком и его команд, а модель программы внутри компьютера будет приспособлена для работы с ней компьютером, а не человеком.

Неужели ты, наконец, разобрался с Coq (Epigram, Agda2 и тп)?

Здравствуйте, thesz, Вы писали:

T>Неужели ты, наконец, разобрался с Coq (Epigram, Agda2 и тп)?

Я вижу, ты так и не понял, о чём я писал.
Может Agda2 доказать, что в этом коде не будет NulPointerException?

if (this.a != null)
  this.a.foo();

Доказательство этого требует дополнительного знания, исполняемся мы в single-threaded или multi-threaded режиме.
А это указываетя где-то в другом месте. Скажем, в коммандной строке компилятора.
И после всего этого, пусть мы попросили компьютер скомпилировать этот код в multi-threaded режиме, agda2 перепишет
этот код как

var tmp = this.a;
if (tmp != null)
  tmp.foo();

или ей слабо? Я не говорю о выдаче ошибки или предупреждений. Я о реакции компьютера на просьбу создать максимально safe код при таких-то условиях выполнения программы.
Вот когда они это научатся делать — тогда будем с ними разбираться.

T>>Неужели ты, наконец, разобрался с Coq (Epigram, Agda2 и тп)?
M>Я вижу, ты так и не понял, о чём я писал.
M>Может Agda2 доказать, что в этом коде не будет NulPointerException?
M>Вот когда они это научатся делать — тогда будем с ними разбираться.

Да умеют они так, умеют. Причём не ad hoc методами.

Видимо, ты так и не понял, зачем Agda2/Coq.

А с твоими творениями мы будем разбираться, когда у них будет основа не хуже, чем у Agda2/Coq.

Здравствуйте, thesz, Вы писали:

T>Да умеют они так, умеют. Причём не ad hoc методами.

Ну покажи, где они это умеют. Цитатку там, документик, можешь сам код наваять.

M>

M>var tmp = this.a;
M>if (tmp != null)
M>  tmp.foo();
M>

А разве это безопасный код? В той же самой Яве компилятор может убрать лишнию переменную

Здравствуйте, avpavlov, Вы писали:

A>А разве это безопасный код? В той же самой Яве компилятор может убрать лишнию переменную

Безопасный. Компилятор всё может, в том числе и ошибаться.

T>>Да умеют они так, умеют. Причём не ad hoc методами.
M>Ну покажи, где они это умеют. Цитатку там, документик, можешь сам код наваять.

Я ж тебе приводил. Ты даже отвечал.

Ну, вот ради прикола, как у тебя будет записано доказательство коммутативности какой-либо операции?

Здравствуйте, thesz, Вы писали:

M>>Ну покажи, где они это умеют. Цитатку там, документик, можешь сам код наваять.

T>Я ж тебе приводил. Ты даже отвечал.

Не помню такого. И такого я бы не забыл. Ты либо меня с кем-то путаешь (может с MPS-овцем каким), либо не о том говоришь.
Я тебя спрашиваю следующее — Coq, Agda2 — это доказатели теорем, доказатели каких-то свойство программы (используя систему типов); но могут ли они модифицировать код так, чтоб он удовлетворял заданным свойствам программы? Я этого нигде в них не нашёл. Вот ссылку на это я с тебя и прошу.

M>>>Ну покажи, где они это умеют. Цитатку там, документик, можешь сам код наваять.
T>>Я ж тебе приводил. Ты даже отвечал.
M>Не помню такого. И такого я бы не забыл. Ты либо меня с кем-то путаешь (может с MPS-овцем каким), либо не о том говоришь.
M>Я тебя спрашиваю следующее — Coq, Agda2 — это доказатели теорем, доказатели каких-то свойство программы (используя систему типов); но могут ли они модифицировать код так, чтоб он удовлетворял заданным свойствам программы? Я этого нигде в них не нашёл. Вот ссылку на это я с тебя и прошу.

Выдачу кода надо писать.

Однако, в отличии от твоей системы, меньше вероятность ошибки и выше уровень описания. Это я про анализ и преобразования.

Что мне ещё подумалось.

Ты апеллируешь к самым низким программистским чувствам — в начале этой нитки ты апеллировал к чувству страха "будет ли у меня тут null pointer exception".

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

Это шутка, конечно, но с правдой на девять десятых вместо обычной доли.

Здравствуйте, thesz, Вы писали:

T>Выдачу кода надо писать.

Ну хорошо, пусть писать. Но где у них система поиска решения, что именно нужно поменять? Не доказать правильно/неправильно, а сказать — вот если тут поменять, то будет правильно.

T>Однако, в отличии от твоей системы, меньше вероятность ошибки и выше уровень описания. Это я про анализ и преобразования.

Неверно. В SymADE вообще сейчас нет никакого уровня и вероятности ошибки, поскольку никакого формализма в основу не положено.
Хочешь — пиши плагин проверяющий такие-то свойства ad hoc, хочешь — используй Coq для проверки этих свойств.
А уровень описания у меня заведомо выше. По той причине, что задача решается в терминах, максимально соответствующих решаемой задаче.

T>Что мне ещё подумалось.
T>Ты апеллируешь к самым низким программистским чувствам — в начале этой нитки ты апеллировал к чувству страха "будет ли у меня тут null pointer exception".
T>Я думаю, что игра на таких низких чувствах не может возвысить ни сам инструмент, ни его автора, ни, тем более, его пользователя.
T>Это шутка, конечно, но с правдой на девять десятых вместо обычной доли.

Посмотри в зеркало.
Ты сам аппелируешь к этим чувствам, рассказывая, что формальная логика гарантирует нахождение ошибок. Сам в это веришь и хочешь уверить других. Вот возьмут они волшебный Coq, и найдёт он им все ошибки в программе. Хотя найти их и доказать правильность/неправильность программы он может только в отношении тех свойств программы, которые его запрограммировали искать. Запрограммируют искать null pointer — будет что-то анализировать и доказывать. Не запрограммируют — он скажет, что ошибки в программе нет. Запрограммируют искать для single-thread модели — будет пропускать ошибки возникающие в multi-thread модели. И по этой причине никакой у них анализ не лучше и не более общий. Потому как все эти свойства, которые от него требуют доказать — тоже доказываются на основе ad hoc моделей. Как в том примере, что ты мне давал для анализа и гарантии невозникновения блокировки программы из-за взаимных локов. Там они взяли и придумали ad hoc модель — все локи должны быть сравнены по приоритету, и тогда можно эти приоритеты сравнить и что-то доказывать. А если локи нельзя сравнить по приоритету — то извините, алгоритм не работает. И чем их работа, постоенная на введении специальных типов для анализа этих свойств, лучше, чем возможность ввести специальные семантические понятия и их анализировать той-же логикой — для меня загадка.

T>>Выдачу кода надо писать.
M>Ну хорошо, пусть писать. Но где у них система поиска решения, что именно нужно поменять? Не доказать правильно/неправильно, а сказать — вот если тут поменять, то будет правильно.

Так это типами ограничивается.

Например, выкинуть просто так a <- b+c нельзя, надо доказать, что смысл программы не поменяется.

T>>Однако, в отличии от твоей системы, меньше вероятность ошибки и выше уровень описания. Это я про анализ и преобразования.
M>Неверно. В SymADE вообще сейчас нет никакого уровня и вероятности ошибки, поскольку никакого формализма в основу не положено.

Это ты какую-то глупость говоришь, да. То, что никакого формализма нет, не означает, отсутствия уровня или вероятности ошибки.

M>Хочешь — пиши плагин проверяющий такие-то свойства ad hoc, хочешь — используй Coq для проверки этих свойств.

То есть, можно обойтись без SymADE? Ура!

SymADE — самая мощная система в мире!!! Она может всё, даже когда её не применяешь, а пользуешься Coq!!!

M>А уровень описания у меня заведомо выше. По той причине, что задача решается в терминах, максимально соответствующих решаемой задаче.

То есть, уровень есть и он выше.

"Мы в восхищении!" (С)МиМ

Ну, так покажи, как проверить (или доказать) коммутативность какой-либо бинарной операции над произвольным типом данных.

T>>Что мне ещё подумалось.
T>>Ты апеллируешь к самым низким программистским чувствам — в начале этой нитки ты апеллировал к чувству страха "будет ли у меня тут null pointer exception".
T>>Я думаю, что игра на таких низких чувствах не может возвысить ни сам инструмент, ни его автора, ни, тем более, его пользователя.
T>>Это шутка, конечно, но с правдой на девять десятых вместо обычной доли.
M>Посмотри в зеркало.
M>Ты сам аппелируешь к этим чувствам, рассказывая, что формальная логика гарантирует нахождение ошибок. Сам в это веришь и хочешь уверить других. Вот возьмут они волшебный Coq, и найдёт он им все ошибки в программе. Хотя найти их и доказать правильность/неправильность программы он может только в отношении тех свойств программы, которые его запрограммировали искать. Запрограммируют искать null pointer — будет что-то анализировать и доказывать. Не запрограммируют — он скажет, что ошибки в программе нет. Запрограммируют искать для single-thread модели — будет пропускать ошибки возникающие в multi-thread модели. И по этой причине никакой у них анализ не лучше и не более общий. Потому как все эти свойства, которые от него требуют доказать — тоже доказываются на основе ad hoc моделей. Как в том примере, что ты мне давал для анализа и гарантии невозникновения блокировки программы из-за взаимных локов. Там они взяли и придумали ad hoc модель — все локи должны быть сравнены по приоритету, и тогда можно эти приоритеты сравнить и что-то доказывать. А если локи нельзя сравнить по приоритету — то извините, алгоритм не работает. И чем их работа, постоенная на введении специальных типов для анализа этих свойств, лучше, чем возможность ввести специальные семантические понятия и их анализировать той-же логикой — для меня загадка.

Сейчас мы зададим тебе вопрос на миллион долларов.

Оба вопроса связаны с распараллеливанием.

Сперва вопрос попроще. Долларов, эдак, тыщ на девятьсот девяносто с половиной.

Как известно, коммутативно-ассоциативные операции легко распараллеливаются.

Например, суммирование: вместо последовательного суммирования по одному элементу массива за раз, мы можем просуммировать левую половину параллельно с правой половиной, а потом их сложить.

Это доступно во всех stream-kernel параллельных системах, например, BrookGPU. Однако в них это свойство необходимо держать в голове программисту, сама система ничего не подскажет. Так и останется программа либо недопараллельной, лиоб излишне параллельной.

Вопрос: как в SymADE доказать коммутативность и ассоциативность некоторой операции?

В Agda2 это входит в набор примеров.

Приведи пример, как это будет описано в SymADE. Текст, весь, от начала до конца. Чтобы мы могли сравнить с текстом на Agda2.

Теперь вопрос посложней. Как раз на миллион долларов ровно.

Вот программа сортировки пузырьком:

void bubble_sort(int* arr, int len) {
    int i,j;
    for (i=0;i<len-1;i++) {
        for (j=0;j<i;j++) {
            if (arr[j] > arr[j+1]) {
                int t = arrj[j];
                arr[j] = arr[j+1];
                arr[j+1] = t;
            }
        }
    }
} /* bubble_sort */

Она настолько не параллельна, насколько это возможно.

Прошу указать, какие изменения в коде этой программы необходимо сделать, чтобы программа сортировки пузырьком стала параллельной и что надо сделать в SymADE, чтобы реализовать все эти преобразования. Для SymADE прошу привести полный текст.

Вот эти два вопроса меня и волнуют.

Причем, второй вопрос действительно может принести миллион — это автоматическое распареллеливание, горячая тема.

T>Вот программа сортировки пузырьком:

Я её поправил.

T>

T>void bubble_sort(int* arr, int len) {
T>    int i,j;
T>    for (i=len-1;i>1;i--) {
T>        for (j=0;j<i;j++) {
T>            if (arr[j] > arr[j+1]) {
T>                int t = arrj[j];
T>                arr[j] = arr[j+1];
T>                arr[j+1] = t;
T>            }
T>        }
T>    }
T>} /* bubble_sort */
T>

Но она всё равно не параллельна.

Здравствуйте, thesz, Вы писали:

T>>>Выдачу кода надо писать.
M>>Ну хорошо, пусть писать. Но где у них система поиска решения, что именно нужно поменять? Не доказать правильно/неправильно, а сказать — вот если тут поменять, то будет правильно.

T>Так это типами ограничивается.

Нет, это не типами ограничивается.

T>Например, выкинуть просто так a <- b+c нельзя, надо доказать, что смысл программы не поменяется.

Вот именно. Смысл. В приведённом мной примере (с null) поведение программы меняется, при использовании временной переменной.
Программа начинает себя вести по другому, она не будет бросать NPE, а в исходном варианте она могла его бросать.
Компилятор не вправе делать подобное кэширование (если это не оговорено в спецификации, в яве, кстати, оговорено, что компилятор
может делать такую оптимизацию, а может и не делать). Потому как оно меняет поведение программы.
Но по смыслу, который вкладывает программист в программу — подобное преобразование кода не меняет смысла программы. Программисту
не нужно там иметь exception. А бывают ситуации, когда программист именно хочет иметь exception.
Сейчас компиляторы ограничены формальными правилами — программа не должна менять своего поведения при оптимизации. Это и ставит
предел возможности автоматизации работы программиста компьютером. Это и есть предел задаваемый монологом.
Если же перейти к пониманию компьютером смысла программы, то он сможет автоматизировать частично (а в будущем практически полностью)
процесс кодирования. Но вот именно смысл и нужно вложить в компьютер, а не формальное соответствие скомпилированной программы коду
вбитому программистом.

T>>>Однако, в отличии от твоей системы, меньше вероятность ошибки и выше уровень описания. Это я про анализ и преобразования.
M>>Неверно. В SymADE вообще сейчас нет никакого уровня и вероятности ошибки, поскольку никакого формализма в основу не положено.

T>Это ты какую-то глупость говоришь, да. То, что никакого формализма нет, не означает, отсутствия уровня или вероятности ошибки.

Чукча не читатель? Я не пишу про то, что формализма нет. Я пишу о том, что он не предопределён и не фиксирован.
Возожность использовать разный формализм и отсутствие его — это не одно и то-же.

M>>А уровень описания у меня заведомо выше. По той причине, что задача решается в терминах, максимально соответствующих решаемой задаче.

T>То есть, уровень есть и он выше.

Программист задаёт понятия, в которых может программировать. Следовательно, уровень абстракции задаётся программистом.
Захочет — может писать на ассеблере. Захочет — на хаскеле. Захочет — в терминах максимально близких к решаемой задаче.

T>Ну, так покажи, как проверить (или доказать) коммутативность какой-либо бинарной операции над произвольным типом данных.

Зачем? Тебе это ничего не скажет о SymADE, поскольку он не предназначен для этих проверок и доказательств.
В хаскеле правильность определения/поведения монады компилятором не проверяется. Он просто компилирует код так, как будто-бы код для монады определён правильно.
SymADE позволяет определять и использовать произвольные новые понятия. А доказывать правильность их определения или использования он не может и не должен.

Здравствуйте, thesz, Вы писали:

T>Оба вопроса связаны с распараллеливанием.

T>Вопрос: как в SymADE доказать коммутативность и ассоциативность некоторой операции?

А как это сделать в Notepad?

T>Приведи пример, как это будет описано в SymADE. Текст, весь, от начала до конца. Чтобы мы могли сравнить с текстом на Agda2.

Например, это можно сделать определив набор понятий (онтологию) аналогичную онтологии Agda2, написать этот код, сделать экспорт в исходный код на Agda2, и запусть их компилятор. Можно и посложнее — переписав компилятор Agda2, чтоб он на вход принимал своё AST дерево, а не обязательно текстовые исходники. Тогда шаг с экспортом можно пропустить.

T>Теперь вопрос посложней. Как раз на миллион долларов ровно.

T>Вот программа сортировки пузырьком:
T>Она настолько не параллельна, насколько это возможно.

T>Прошу указать, какие изменения в коде этой программы необходимо сделать, чтобы программа сортировки пузырьком стала параллельной и что надо сделать в SymADE, чтобы реализовать все эти преобразования. Для SymADE прошу привести полный текст.

Для начала, в С нет понятия параллельного вычисления. В языке. Чтоб что-то распараллеливать, нужно это уметь делать. То есть в С надо добавить возможности параллельного выполнения кода. Вот это SymADE может сделать. К онтологии языка С добавить новые понятия, нужные для параллельного выполнения кода. Выполнить параллельно, подождать когда параллельный процесс закончится и так далее. Понятно, что ради конкретного пузырька с этим возиться не стоит. Мета-программирование — оно для больших проектов и сложных задач. Не алгоритмически сложных, а сложных для понимания (охвата) человеком.
Чтоб привести тебе полный текст этого дополнения, надо вначале полностью определить онтологию для С, а я замахаюсь это делать сейчас. Я ещё с явой не закончил (то есть её ещё не удобно редактировать, и пока я не доделаю редактор — за другие языки браться не буду).

В конце той статьи, с которой началось обсуждение, я написал, что задача по созданию ИИ, который будет заниматься поиском новых знаний среди уже определённых понятий — в SymADE не реализована, это задача для будущего. Когда закончу с текущими проблемами, буду думать о реализации такого ИИ.

T>Причем, второй вопрос действительно может принести миллион — это автоматическое распареллеливание, горячая тема.

К тому времени, как компьютер научится прилично параллелить код автоматом — это уже будет не актуально
Но об этом в статье уже тоже написано.

Здравствуйте, mkizub, Вы писали:

M>

M>Переход к написанию программы компьютером — это переход от монолога, к диалогу. При этом, так же как и при диалоге человека с человеком, у компьютера должна быть своя, внутренняя модель программы. У компьютера должна быть возможность вводить новые понятия (в терминах которых эта модель и будет выражена). Он будет общаться с человеком (программистом) на некотором языке (языках), достаточно независимом от внутренней модели программы. Эта модель будет изменяться не непосредственно программистом, а в результате диалога между компьютером и программистом. Эти языки общения будут специально приспособлены для удобства понимания человеком и его команд, а модель программы внутри компьютера будет приспособлена для работы с ней компьютером, а не человеком.

Очень сложно понять что ты предлагаешь, если не шарить в этом самому. Я когда-то интересовался MPS, но поскольку на тот момент она была еще сыра, а туториал не соответствовал последней версии продукта, я решил отложить знакомство до «лучших времен».

Главная твоя проблема это то, что ты не можешь толком объяснить свои мысли. Я перечитал несколько тем на RSDN, ixbt, прочитал три твои статьи на developers.org.ua, пробовал найти что-то интересное на твоем сайте запускал программу. Информации много, но все одно и то же. То время, которое ты потратил на общение на форуме можно было бы продуктивнее использовать на написание небольшого документа, от А до Я (правда на developers.org.ua статья хорошая).

Я попытаюсь изложить свое видение материала, а ты, если что не так, подкорректируй меня.

Итак, давайте рассмотрим что же такое процесс программирования, откуда берется задание, как оно представляется в голове у человека и как он его «скармливает» компьютеру в виде программы.
1. Результатом ознакомления и обработки технического задания является некая модель, выраженная совокупностью понятий и связей между ними. Причем эти понятия, зачастую, высокоуровневые. Например

«Система должна позволять менять параметры А, В и С».

2. Далее происходит постоянный процесс конкретизации параметров.

Параметры А, В, С будут храниться в базе данных, и редактироваться пользователем с помощью графического интерфейса
 
Параметры А, В, С будут храниться в таблице Т, редактироваться в окне «Свойства» приложения «Администрирование»

Параметры А, В, С будут храниться в таблице Т, будут представлены строковыми параметрами, 
редактироваться в окне «Свойства» приложения «Администрирование». 
Параметры А и В будут выбираться из ComboBox, паратетр С будет вводиться врочную в компоненте EditBox

И так далее... По сути это выражение одних понятий с помощью других.
3. В конце концов этот процесс заканчивается построением абстракций (классов и интерфейсов) и имплементацией функциональности. В результате мы получаем набор понятий и связей между ними (сравните с пунктом 1), но набор понятий ограничен такими как «класс», «интерфейс», «метод», «переменная» итд, то есть тем, что нам предоставляет язык программирования.
4. Компилятор (интерпретатор) обрабатывает текст программы, находит синтаксические ошибки, оптимизирует код, предупреждает о возможных логических ошибках итд.

И так, что мы имеем на сегодняшний день? Компьютер вовлечен только в стадию 4, Современные IDE, редакторы форм, плагины пытаются работать на уровне 3, но только если этот уровень ясно определен (например ИДЕ работает с языком программирования, редактор форм — с библиотекой построения графического интерфейса, плагины — с другими популярными и устоявшимися библиотеками)
По сути работа программиста заключается в том, чтобы выразить понятия, которыми оперирует человек, понятиями, которыми оперирует компьютер.
Вы можете возразить: с приходом ООП мы оперируем не понятиями языка программирования а конкретными классами. Например понятие «окно» выражается классом «Window», «кнопка» — «Button», «строка меню» — «Menu». Но ведь компьютер (компилятор) — работает все теми же классами, операторами и методами. Он не имеет информации о том, как связаны Button и Window. Этим и ограничивается автоматизм.

MPS пытается решить проблему путем расширения набора конструкций языка, расширением синтаксиса (то есть сделать класс Window частью языка, зарезервировать для него ключевое слово; добавить в язык дополнительные операции, удобные для редактирования графического интерфейса).

SOP же предлагает автоматизировать этап 2 (т.е. процесс конкретизации понятий). Ведь выражение одних понятий с помощью других это и есть то самое программирование в форме диалога.

Для лучшего понимания разницы между SOP, MPS и традиционным программированием давайте рассмотрим следующую метафору.

Представьте себе некий отчет, который оформлен в виде HTML файла. Отчет предоставляет итоговую информацию о деятельности некоторого предприятия. Чтобы подчеркнуть принадлежность данных к разным категориям используется форматирование.

Отчет
приход
    прибыль от продаж 200
расход
    на рекламу        30
    на зарплату        60
    налоги            40
инвестиции
    транспорт        20
    оборудование        50

Это аналог традиционного программирования. Если мы захотим что-то поменять, (ну например, разукрасить всё в разные цвета), мы должны править сам документ, таблицу стилей, сделать рефакторинг (для каждого раздела добавить свой стиль) итд.

Подход MPS: давайте расширим HTML (аналог написания DSL) а к нему напишем свой редактор и компилятор, переводящий данные на нашем языке в обычный HTML. Тогда меняя свой язык мы сможем легко и просто решать трудные задачи.

Подход SOP: а давайте все забабахаем в XML, при этом каждое число будет иметь свой смысл и явно будет прописано что оно значит. Что-то типа такого:

<section description = «прибыль» type=«income»>
    <value type=«sales» description = «продажи»>200</revenue>
</section>
<section description = «расход» type=«cost»>
    <value type=«advertisement» description = «реклама»>30</revenue>
    <value type=«salary» description = «зарплата»>60</revenue>
</section>
<section description = «инвестиции» type=«investment»>
    <value type=«transport» description = «транспорт»>20</revenue>
</section>

Теперь мы можем сгенерить HTML, doc, rtf, pdf, jpeg, avi, ppt, сколько есть фантазии.... Мы можем редактировать данные как вручную, так и наваять програмку или вообще создать целый комплекс документооборота.
Использование XML это один из способов семантической организации данных. Вопрос: почему бы не использовать такой же способ для написания программ? Для этого нужно чтобы компилятор (точнее IDE) понимал семантику, а не набор команд и интерфейсов.

T>>Приведи пример, как это будет описано в SymADE. Текст, весь, от начала до конца. Чтобы мы могли сравнить с текстом на Agda2.
M>Например, это можно сделать определив набор понятий (онтологию) аналогичную онтологии Agda2, написать этот код, сделать экспорт в исходный код на Agda2, и запусть их компилятор. Можно и посложнее — переписав компилятор Agda2, чтоб он на вход принимал своё AST дерево, а не обязательно текстовые исходники. Тогда шаг с экспортом можно пропустить.

Вопрос был — "как сделать это средствами SymADE", а не как задействовать Agda2 или её логику.

Иными словами, толком ты ответить не можешь. У тебя всё сводится к "в SymADE всё можно написать". Так это и на ассемблере можно.

T>>Теперь вопрос посложней. Как раз на миллион долларов ровно.
T>>Вот программа сортировки пузырьком:
T>>Она настолько не параллельна, насколько это возможно.
T>>Прошу указать, какие изменения в коде этой программы необходимо сделать, чтобы программа сортировки пузырьком стала параллельной и что надо сделать в SymADE, чтобы реализовать все эти преобразования. Для SymADE прошу привести полный текст.
M>Для начала, в С нет понятия параллельного вычисления. В языке. Чтоб что-то распараллеливать, нужно это уметь делать. То есть в С надо добавить возможности параллельного выполнения кода. Вот это SymADE может сделать. К онтологии языка С добавить новые понятия, нужные для параллельного выполнения кода. Выполнить параллельно, подождать когда параллельный процесс закончится и так далее. Понятно, что ради конкретного пузырька с этим возиться не стоит. Мета-программирование — оно для больших проектов и сложных задач. Не алгоритмически сложных, а сложных для понимания (охвата) человеком.

"Конкретный пузырёк" — это сложный пример для современных систем автоматического распараллеливания. Такие вещи мало, кто умеет делать.

M>Чтоб привести тебе полный текст этого дополнения, надо вначале полностью определить онтологию для С, а я замахаюсь это делать сейчас. Я ещё с явой не закончил (то есть её ещё не удобно редактировать, и пока я не доделаю редактор — за другие языки браться не буду).

Иными словами, работать с SymADE очень сложно. Настолько, что ты не можешь выдать ни одного решения ни одной выдаваемой тебе задачи за приемлемое время.

Причем задачи не включают в себя пользовательский интерфейс, базы данных и прочее, для чего надо пыхтеть и стараться. Надо просто собрать правильную логику.

И даже на это тебя не хватает.

А ведь ты автор SymADE, ты умеешь работать с ней лучше кого-либо другого, и даже лучше практически всех, кто станет её использовать (первое время, по крайней мере).

Вот я и думаю. Приду я на работу, начну читать про SymADE, ко мне подойдёт начальник, спросит, что такое, а я ему в ответ: это штука, об идеях которой можно писать длинные статьи и которая отлично подходит для оправдания ничегонеделания, поскольку ничего с её помощью сделать невозможно. Даже миллион баксов заработать. Предвижу несомненное повышение уважения ко мне со стороны коллег.

M>В конце той статьи, с которой началось обсуждение, я написал, что задача по созданию ИИ, который будет заниматься поиском новых знаний среди уже определённых понятий — в SymADE не реализована, это задача для будущего. Когда закончу с текущими проблемами, буду думать о реализации такого ИИ.

Eurisko. Конец 70-х. Её натравили на открытие знаний в области математики — задали несколько аксиом и отправили в путь. Она сама открыла понятие простых чисел, что-то ещё (теорему Пифагора, по-моему), а потом начала открывать бессмысленные связи, никому не нужные. И это ей ещё Ленат помогал, вручную.

Those who do not understand are doomed to reinvent, poorly.

T>>Причем, второй вопрос действительно может принести миллион — это автоматическое распареллеливание, горячая тема.

M>К тому времени, как компьютер научится прилично параллелить код автоматом — это уже будет не актуально

Этим занимаются не компьютеры, а люди. Современные алгоритмы вполне сравнимы с ручным распараллеливанием.

M>Но об этом в статье уже тоже написано.

И совершенно неправильно написано.

Ты пишешь о том, что ты толком не знаешь. Не о реальных проблемах, а о своих о них представлениях.

Чего стоит упоминание о null pointer exception. Про них уже все давно забыли, все работают уровнем выше (или стремятся забыть и работать). А ты всё ещё про них думаешь.

Здравствуйте, thesz, Вы писали:

T>Вопрос был — "как сделать это средствами SymADE", а не как задействовать Agda2 или её логику.

Это и есть "средствами SymADE". SymADE — это среда разработки программ, а не ещё один язык программирования, который должен решить все проблемы человечества.

T>Иными словами, толком ты ответить не можешь. У тебя всё сводится к "в SymADE всё можно написать". Так это и на ассемблере можно.

Иными словами, ты не можешь воспринять ничего нового. Ты можешь только свести информацию к уже привычным, уже известным тебе понятиям. И не понимаешь, что при этом всё новое в информации теряется.
Ну не сводятся законы квантовой механики к привычной нам законам макро-физики. Их надо просто выучить, как есть, не сводя к привычной механике.
Ты пытаешься свести SymADE к языкам программирования. Не надо. Это не приведёт тебя к пониманию. Разве ты только хочешь удостовериться, что в SymADE ничего нового нет, и удовлетворённо пребывать в этом мнении. И к простому редактору это свести нельзя. И к простому мета-программированию нельзя. В SymADE есть эти элементы, но к набору этих элементов он не сводится.

Нельзя на ассемблере всё написать. Практически, на практике нельзя. Не хватит всех ресурсов, всех программистов в мире, на то, чтоб написать даже базовый софт на ассемблере.

T>>Вопрос был — "как сделать это средствами SymADE", а не как задействовать Agda2 или её логику.
M>Это и есть "средствами SymADE". SymADE — это среда разработки программ, а не ещё один язык программирования, который должен решить все проблемы человечества.

Иными словами, SymADE выступает здесь в роли посредника. Паразита. Тратя на себя внимание и не принося ничего полезного.

T>>Иными словами, толком ты ответить не можешь. У тебя всё сводится к "в SymADE всё можно написать". Так это и на ассемблере можно.
M>Иными словами, ты не можешь воспринять ничего нового. Ты можешь только свести информацию к уже привычным, уже известным тебе понятиям. И не понимаешь, что при этом всё новое в информации теряется.

Я не могу воспринимать ничего, что не упрощает для меня работу.

M>Ну не сводятся законы квантовой механики к привычной нам законам макро-физики. Их надо просто выучить, как есть, не сводя к привычной механике.

Это ты глупость говоришь, как всегда.

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

Так и тут, в программировании, есть Lambda the Ultimate Imperative, сводящая воедино два формализма.

Поэтому, мил человек, потрудись и сведи SymADE к одному из формализмов. Хотя бы одному.

M>Ты пытаешься свести SymADE к языкам программирования. Не надо. Это не приведёт тебя к пониманию. Разве ты только хочешь удостовериться, что в SymADE ничего нового нет, и удовлетворённо пребывать в этом мнении. И к простому редактору это свести нельзя. И к простому мета-программированию нельзя. В SymADE есть эти элементы, но к набору этих элементов он не сводится.

Синергия, значит.

Синергии работают только в грёзах менеджеров.

Если целое не равно сумме своих частей, то целое, наиболее вероятно, меньше суммы своих частей.

Из чего я предполагаю, что если я возьму части SymADE по отдельности — отдельно язык программирования, отдельно редактор, отдельно система метапрограммирования, — то я получу то же самое, но лучше (мощнее, быстрее и тп).

Доказательств обратного я не вижу.