Без заголовка

Итак, тяжёлую работу формального/строгого/точного рассуждения/вывода/inference будут делать компьютеры, а от людей потребуется только знание математической, физической и так далее (дисциплин интеллект-стека, а затем инженерной, менеджерской, предпринимательской) онтологии с типами, соответствующими объектам внимания. Для наших целей усиления интеллекта достаточно соответствующей предметной интуиции для приблизительных/интуитивных рассуждений с этими объектами внимания, чтобы высказывать догадки. А проверять эти догадки сможет и компьютер, никаких тут вопросов. Как оптимист, который занимается формальной инженерией, скажу Вам, что Вы очень сильно оптимистичны :). Но это хорошо :). Если бы я знал насколько это все сложно, то не уверен, что стал бы в это ввязываться. Хотя я уже не схожу с ума от сложности, что тоже неплохо — теперь это для меня просто сложная работа. Но зато ответу можно доверять, он точный/строгий/формальный. По большому счёту, ровно вот это называется "точными науками". Не совсем так. Всегда есть Trusted computing base. Т.е. всегда есть куча всего чему мы (почему-то) доверяем, ну и мы можем доверять результату покуда мы верим в TCB. В контексте (системно-)инженерного подхода очень полезно отслеживать список того, чему мы вынуждены доверять. Ну и о прогрессе можно судить о сокращении этого списка путем перевода частей TCB в строгие формальные теоремы. Type theory тут удобен, ибо можно организовать формальный девелопмент в виде Directed Acyclic Graph'а, что имхо довольно-таки системно-инженерно :). Исходными узлами будут базовые и вспомогательные допущения, а всякие теоремы/леммы переводят все в конечные утверждения. TCB удобно разбить на три части: - базовые поверья мета-уровня, которые мы обычно не трогаем: hardware, compiler, proof checker, какие-то совсем уж базовые аксиомы и мета-теоремы. Компилятор иногда можно вынести из TCB, но проблема в том, что proof checker тоже написан на каком-то языке, т.е. на 100% все-таки нельзя. Разве что в машинных кодах написать, но тут размер TCB фактически вырастет — доверять машинному коду будет сложновато. - основные допущения — от них тоже не избавиться. В случае adversary моделей, мы делаем допущения об ограничения adversary power. Без этого никак, ибо если их нет, адверсари победит :). Насколько модель ограничений адверсари адекватна? К примеру, изобретение квантового компьютера может их часто инвалидировать, в большей части криптографии это может быть актуально. Но как правило эти допущения можно видоизменять. Т.е. даже если допустить P=NP, то степень полинома в P может быть все равно большая, так что не факт что адверсари это сильно поможет, особливо если подправить параметры. - ну и какие-то рабочие допущения, на которые мы пока опираемся, но надеемся устранить в перспективе (если хватит бюджета, мозгов, сил и проч).