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

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


D>А что, собственно, ты называешь "высокоуровневый язык"?
D>Например, C++ это высокоуровневый язык? Или это такой же ассемблер как HOL. Собственно в чем разница между C++ и ассеблером. Разница в том, что к C++ прилагается компилятор, который кострукции языка умеет отображать в ассемблер. Тогда, по аналогии, HOL — не ассемблер (ассемлер в чистом виде это определение доказательства, как последовательности из формул, в которой каждая следующая получается применением правил вывода к предыдущим). И хотя идеологически HOL внутри это именно это определение и есть, то для пользователя, HOL идет вместе со свякими политиками применения правил вывода т.е. средством отобраения твоих "высокоуровневых идей" в "доказательство по определению".

"доказательство по определению": должен быть уровень "ассемблерный" , но переносимый (между hol , coq и тп). чтоб теоремы можно было скачивать из интернета и легко с помощью компа проверять правильность выкладок.

"высокоуровневых идей": а тут всё должно быть удобнее чем C# и дебагер в visual studio 2005.

иногда хочется видеть(понимать) всё вместе —
не хватает аналога uml ( в придачу можно написать книгу "рефакторинг: улучшение существующи матем теорий" )


> Так же к HOL прилагается ML, на котором ты можешь написать свои собственные патерны, и способы "отображения идей". И получается, что HOL, идет вместе с тем, что программисты называют мета-программированием.

D>Или под "высокоуровневым языком" ты понимаешь что-нить типа managed? Т.е. язык который, кроме отображения в ассемблер предлагает, что-то новое, не существующее на уровне процессорных команд.

когда я читаю книгу по матану, но я много о чём не думаю. хотя вроде теже самые процессорные команды.

> [....]


короче всё смешно и интересно.