Видео будет?

Все материалы будут в свободном доступе.

СлабО доказать теорему о выполнении неформальных и мутных требований заказчика «еще вчера», и чтоб потом любая мартышка могла решение поддерживать?

Академики не нужны. Пожирателям грантиков и мамкиного борща давно пора на свалочку истории.

Ха ха, если б не «пожиратели грантиков» ты ба щас с дубиной бегал в Африке, а не за компом сидел, говнокомменты постил.

Действительно, невнимательно прочитал новость.

просто спрошу с претензией на собственное понимание... Пролог? ) или сугубо теоретический аппарат?

Coq, Agda, Prolog (PPTP, SATCHMO) или что-то ещё?

Академики не нужны.

Кто нужен? PHP быдлокодеры?

В индустрии используется HOL, как я понимаю.

В их индустрии, то бишь в Intel-е.

Ого, зашёл на ЛОР!

Спасибо за новость. Давно хотелось получить какое-нибудь введение в область автоматизации математики.

Жаль, что не в МИАН'е или НМУ. Санкт-Петербургу повезло.

Тебя дезинформировали. Пожиратели борщика и грантиков никогда ничего полезного не делали, за всю богатую историю человечества. Все достижения прогресса это дело рук практиков.

Почитай лекции этого самого Харрисона - там он на говно-ML-чеге говнотеоремки говнодоказывает. И говнонедопроложек пишет.

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

У них есть несколько интересных статей (помню только названия, ссылок дать сейчас не могу, но оно все легко гуглится):

• Intel's Successes with Formal Methods
• Fifteen Years of Formal Property Verification in Intel
• Formal Methods at Intel — An Overview

Любые практические решения являются реализацией теоретических изысканий.

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

Толсто. Этот твой «любой инженер» придумал бы SQL без д-ра Кодда с его реляционными алгебрами? Ничего, что компилятор написать невозможно, не пользуясь теорией формальных языков, которая является одним из разделов матлогики?

вам больше повезло. в питере нет нму

1) Реляционки - зло и должны умереть. Теоретики должны вечно гореть за это в аду.

2) Никакая такая «теория формальных языков» даром не нужна. Все эти убогие автоматы, LALR и тому подобная чушь в реальной практике не используется никогда. Все настоящие компиляторы - на вручную написанном recursive descent, без всякой там дебильной теории, в лоб, по-инженерному.

Ну да, кто головой думает, получает больше, чем глупая мартышка, которая «работу работает». В этом плане я ваше негодование понимаю, конечно.

Любые практические решения являются реализацией теоретических изысканий.

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

Кто «головой думает» вместо того, чтобы работу работать, хлебает мамкин борщик или дерется с другими такими же «думающими» за огрызки грантиков. В то время как все реальные деньги достаются практикам.

Никакая такая «теория формальных языков» даром не нужна. Все эти убогие автоматы, LALR и тому подобная чушь в реальной практике не используется никогда. Все настоящие компиляторы - на вручную написанном recursive descent, без всякой там дебильной теории, в лоб, по-инженерному.

Ну да. Грамматики не нужны, регулярные выражения не нужны, обоснование корректности программ не нужно...

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

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

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

Такие инженеры-практики заканчиваются тогда, когда задача становится достаточно сложной, чтобы обойтись простой интуицией.

Ну да. Грамматики не нужны,

Формальные - не нужны. Есть неформальные, не особо вообще формализуемые, но гораздо более практичные PEG.

регулярные выражения не нужны

Именно так, не нужны, есть PEG.

обоснование корректности программ не нужно...

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

Без теории реализация является кучей наспех подогнанных костылей без чёткого подхода к архитектуре и неэффективными алгоритмами.

Ололошечки. Архитектура - инженерная дисциплина. Окодемеги за архитектуру не знают вообще ничего. И за эффективность алгоримтов они тоже не в курсе, размахивают своей ненужной O-нотацией, которая разбивается вдребезги о простые инженерные соображения о cache locality.

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

Благодарю покорно, но сортами говна я не интересуюсь.

Такие инженеры-практики заканчиваются тогда, когда задача становится достаточно сложной, чтобы обойтись простой интуицией.

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

И за эффективность алгоримтов они тоже не в курсе, размахивают своей ненужной O-нотацией, которая разбивается вдребезги о простые инженерные соображения о cache locality.

Обалдеть.

А потом такие как вы пишут тормозной код с асимптотикой O(n^2), когда уже лет 30 как существует алгоритм с лучшим временем работы. «Зато у мну все в кэш влезает, ыыы!»

Есть неформальные, не особо вообще формализуемые, но гораздо более практичные PEG.

Всё с вами ясно, вы не в теме. Ибо PEG очень похожи на КС-грамматики, и очень даже формальны. Но множество языков, ими порождаемых, строго вложено в множество языков, порождаемых КС-грамматиками.

Именно так, не нужны, есть PEG.

S -> FP

P -> palm

F -> face

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

В вашей - не будет. Ибо вы ничерта не знаете, но мнение имеете.

Но множество языков, ими порождаемых, строго вложено в множество языков, порождаемых КС-грамматиками.

Вы редкостно некомпетентны. PEG описывает более широкий класс грамматик.

Инженер ставит эксперименты, и исходит всегда только из фактов.

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

Судя по расписанию лекции будут 28 и 29

Вы редкостно некомпетентны. PEG описывает более широкий класс грамматик.

Ага-ага. Детерминировали КС-грамматику и получили более широкий класс.

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

Советую почитать о структуре человеческих знаний и о том что есть: теоретический(рациональный) уровень и практический(чувственный). Было темное время когда они рассматривались раздельно и каждый пытался доказать что его болото правильнее, но уже давно эти два уровня идут вместе. Нет теории без практики и практики без теории. Теория берется из опытов и подтверждается опытами(в общем), да это так, но и практика берется не только опытным путем, но и путем применения теории.

Вот вам задача: дана сеть дорог, и у каждой дороги пропускная способность установлена, как распределить самым рациональным образом трафик на дороге?

Инженер ставит эксперименты, и исходит всегда только из фактов. [...] Только факты и логика

Логика - инженерная наука?

Напомнило как у нас в универе некоторые пытались определения доказывать.

Кто «головой думает» вместо того, чтобы работу работать, хлебает мамкин борщик или дерется с другими такими же «думающими» за огрызки грантиков. В то время как все реальные деньги достаются практикам.

Питер Норвиг с вами категорически не согласен, гг. Как впрочем и знающие ненужную теории люди вроде того же Шишкина и других. Наверное все они ведущие посты заняли от того что теория не нужна, ага.

ты гониш.

фортран и лисп были написаны крутыми мастерами(практико-теориками) при не существующей на тот момент теории формальных языков.

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

ну не только рекурсивным спуском ручнокодирование ограничивается, в своё время имел преимущества свёртка по таблицам ( хз как это в L|R нотации) т.е когда пихаются токены в стек и постоянно происходит замена того или иного набора верхних элементов на иной набор согласно той самой «таблице»

автокаталитичность «теория»-«практика»-«хрень»

Зачем инженеру заниматься такой непрактичной задачей?

PEG - не КС, а более широкое подмножество recursively enumerable грамматик.

как распределить самым рациональным образом трафик на дороге?

Как раз теоретик тут и обосрется, решая в лоб NP-полную задачу. А практик подберет эвристику попроще. Или вообще ничего сам решать не будет, а вырастит колонию амёб:

http://www.wired.com/wiredscience/2010/01/slime-mold-grows-network-just-like-...

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

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

1. Отличный ответ. Аргументация на высоте.

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

peg!... peg!.. peg!...

Фоннаты Nemerle на ЛОРе?!

Рекурсивные парсеры просты и очевидны, и в теориях не нуждаются. Любой инженер легко допрет на интуиции. Теория формальных языков бесполезна на практике слегка больше чем совсем.

Какое отношение это быдлоподелие имеет к PEG? Они и packrat не осилили, с Праттом своим идиотским носятся, как с обоссанной корзинкой.

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

1) Реляционки - зло и должны умереть. Теоретики должны вечно гореть за это в аду.

1. Отличный ответ. Аргументация на высоте.

Несмотря на аргументацию, позволю себе согласиться с аноном. Страдать синдромом утенка (сиречь - использовать RDBMS только потому что в студенчестве научили РА и Oracle) при внедрении современных требований бизнеса к сложности данных - не комильфо. В таком смысле - да, гореть им в аду.
Но и не буду спорить с тем, что, мол, к примеру, Cassandra, или там Neo4j под собой не имеют никаких формализмов - се глупо.