И что я последнее время все время с Вами спорю :)
Однако, темы Вами предложенные, скорее уже
зарекомендовали себя как тупиковые. (Не относится
к вычислениям с длинными молекулами).
Специалистам как раз ясно, что эти проблемы надо
переформулировать, чтобы их можно было надеятся решить.
Ну о каком формальном доказательстве правильности
программ идет речь, если все интересные свойства
алгоритмически неразрешимы?
Что можно надеяться формально доказать без формальной
спецификации того, что программа должна делать?
Кто такую спецификацию будет писать ? А проверять ?
Это вообще возможно ?
Цитата
Главной цели конечно нет, источником развития (как и всегда) являются практические проблемы, для решения которых надо создавать новые математические понятия и методы. Например, проблемы понимания естественно-языковых текстов, проблемы формального доказательства правильности компьютерных программ, проблемы автоматизации синтеза программ по их спецификациям, проблемы извлечения знаний из больших массивов данных, проблемы предсказания свойств сложных химических соединений (это очень актуально для фармацевтической промышленности), и т.д. и т.п.
