PADL: Machine reasoning about machines: ACL2 theorem prover

In 1989, Boyer and Moore opened an empty Emacs buffer and started a complete re-write of NQTHM. The result is the ACL2 prover. Theorems in NQTHM were expressed as Lisp expressions; the prover itself was written in a home-grown dialect of Lisp, in a largely imperative style. First Boyer and Moore wanted to switch to Common Lisp (CL), so they don't have to maintain their own compiler. Mainly they wanted to re-write the prover in a pure-applicative subset of CL. The major attraction is that the specification and the implementation languages become the same; hence you can use the prover to prove (a part of) itself. It turns out that pure-functional style resulted in a better and a better maintainable code. As J. Moore remarked, his experience of writing and maintaining an imperative prover NQTHM for 18+ years, and similar 11-year experience for the pure-functional ACL2 prover showed the applicative style is better. J. Moore said that he will never go back to the imperative style.

The ACL2 prover is 72KLOC long. The documentations takes 1.7 MB; in addition; comments in the code occupy 1.2 MB. Whenever the authors extent or correct a function, they describe the motivation and the action in the comments. Thus ACL2 comments reflect thirty years of evolution of the theorem provers. The ACL2 home page http://www.cs.utexas.edu/users/moore/acl2 lists two books, several ACL2 workshops. The site contains the full, hyperlinked ACL2 documentation. ACL2 is freely downloadable from the above site.

Достаточно большая программа-то. 72KLOC. Вполне тянет на... ну, на большую программу.

PS
Любая хорошая статья содержит много разной информации.

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

T>... As J. Moore remarked, his experience of writing and maintaining an imperative prover NQTHM for 18+ years, and similar 11-year experience for the pure-functional ACL2 prover showed the applicative style is better. J. Moore said that he will never go back to the imperative style.

Эх. И не говори. Я вот как погляжу на этот гребаный императивный OpenSceneGraph, который я использую для рендера, так сразу грустно становится. Как представлю себе, насколько проще было бы работать с чисто функциональным scene-graph-ом. Ух. Мало того, что было бы проще в разы (мне такой монстр как OSG в принципе-то и не нужен), так еще и быстрее работало бы (гораздо проще было бы применить всякие game specific оптимизации, для которых мега-универсальный OSG не заточен).

Да и в целом, практически везде, функциональный стиль проще. Забили мозги в детстве паскалем/Си/С++. Как подумаешь, что кучи ошибок и сложностей могло бы просто не быть. Р-р-р-р.

V>Да и в целом, практически везде, функциональный стиль проще. Забили мозги в детстве паскалем/Си/С++. Как подумаешь, что кучи ошибок и сложностей могло бы просто не быть. Р-р-р-р.

Во-во.

(одевает шапку старого деда, умудрённого программиста)

Нынешней-то молодёжи все быстродействие подавай. Как бы побыстрей всё вычислить.

В наше-то время мы декларативно писали, на макросах, о быстродействии не заботились. Быстродействия тогда хватало за глаза — ведь всё же на ассемблере писано было. Хоть машины были и не чета нынешним.

Шестнадцати килогерцовый 80(0.5 — читай "половина")86/4!

Внешняя шина данных и адреса в четыре бита, битово порезаная.

А нынешние-то! Копирования боятся! Четыре байта скопировать боятся лишний раз!

Тьфу!

Молодёжь!

(снимает шапку старого деда)

Сколько смотрю, всё сильней убеждаюсь, что основные ошибки из-за решения сиюминутных проблем. "Хватай мешки! Вокзал отходит!"

Примеров обратного мало, но они очень характерные.

Вот из железной же среды пример: DEC Alpha планировался с учётом развития на 20 лет вперёд. И ведь получилось. И ведь конкурентов обгонял на несколько корпусов уже в самом начале пути.

Ан, нет. Будем оптимизировать, что под рукой.

Здравствуйте, thesz, Вы писали:
T>the applicative style is better. J. Moore said that he will never go back to the imperative style.

Простите, а куда я попал? Тут холиварят на тему pure vs impure или declarative vs. imperative?

T>>the applicative style is better. J. Moore said that he will never go back to the imperative style.
MC>Простите, а куда я попал? Тут холиварят на тему pure vs impure или declarative vs. imperative?

А вы, простите, куда попасть собирались?

V>Да и в целом, практически везде, функциональный стиль проще. Забили мозги в детстве паскалем/Си/С++.
Я не писал ничего сложного в чисто функциональном стиле поэтому мне всегда было интересно, действительно ли настройка мозга на чистату не будет для него костылем? Ведь у человека мозг рождается и развивается далеко не в pure world.

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

V>>Да и в целом, практически везде, функциональный стиль проще. Забили мозги в детстве паскалем/Си/С++.
D>Я не писал ничего сложного в чисто функциональном стиле поэтому мне всегда было интересно, действительно ли настройка мозга на чистату не будет для него костылем? Ведь у человека мозг рождается и развивается далеко не в pure world.

т.е. ты умеешь двигать предметы силой мысли?

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

Здравствуйте, BulatZiganshin, Вы писали:
BZ>т.е. ты умеешь двигать предметы силой мысли?

Типа как сайд-эффект мыслительной деятельности?

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

MC>Здравствуйте, BulatZiganshin, Вы писали:
BZ>>т.е. ты умеешь двигать предметы силой мысли?

MC>Типа как сайд-эффект мыслительной деятельности?

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

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

BZ>т.е. ты умеешь двигать предметы силой мысли?
Вроде да, я силой мысли посылаю импульсы в мышцы и двигаю предметы.

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

V>>Да и в целом, практически везде, функциональный стиль проще. Забили мозги в детстве паскалем/Си/С++.
D>Я не писал ничего сложного в чисто функциональном стиле поэтому мне всегда было интересно, действительно ли настройка мозга на чистату не будет для него костылем? Ведь у человека мозг рождается и развивается далеко не в pure world.

Автомобиль — тоже костыль. Однако ездить быстрей, чем ходить пешком.