Скоро новый год и хочется немного помечтать. Что нас ждет в будущем и что хотелось бы получить?
Давайте подумаем в чем суть программирования. Это описание инструкций на неком формальном языке. Но почему только программисты этим занимаются? Как здорово бы было, если бы не только программисты структурировали свои знания и открытия для возможности многократного повторного использования машинным разумом. Давайте рассмотрим примеры.

Математика
Математика — достаточно строгая наука. Когда публикуется доказательство теоремы, то проверяют это доказательство только ученые. В действительности, это можно было бы поручить компьютеру. Логический вывод можно было бы описывать на формальном языке, который бы потом проверял автоматически компьютер.

Вот возьмем, например, теорему Ферма. Она долгое время не имела доказательства. В конце 20-го века ее все-таки доказали, но около пяти лет не могли до конца признать правильность доказательства — слишком уж оно было сложное. Если бы запись доказательства была бы на формальном языке, который бы понимал компьютер, то ждать 5 лет не пришлось бы.

В этом направлении давно уже есть исследования. Есть даже попытки автоматизировать доказательство теорем, чтобы компьютер сам искал доказательство. Я сам будучи студентом писал такую программу, которая делает вывод одной простой теоремы. Но в общем случае компьютер пока еще не может доказывать теоремы. При этом проверка теоремы является более простой задачей, чем ее доказательство. Поэтому задача проверки разрешима уже сейчас, используя текущие возможности компьютеров.

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

Юриспруденция
Законы, кодексы, указы и другие документы обязательного применения часто достаточно сложны. Назовем их все упрощенно законами. Некоторые законы содержат логические формулы, описанные естественным языком. Такие тексты часто понимаются неоднозначно. Некоторые законы противоречат друг другу. Чтобы находить данные противоречия, необходимо обрабатывать довольно большие объемы информации.

Формальный язык в этом случае значительно упростит работу с законами. Можно будет автоматически проверять совместимость закона с другими законами, обнаруживать случаи, которые не покрывает закон. Также на формальном языке можно будет писать список проверок (аналог unit-тестов), которым должен удовлетворять закон и сразу обнаруживать ошибки в поправках к закону. Можно будет перестать кормить огромную армию юристов, которые зарабатывают на этих знаниях. А это огромная экономия для всей страны.

Итог
Не знаю, когда наступит это светлое будущее, но я в него верю. Разумеется, профессионалы в своей области не останутся без работы. Просто их работа перейдет на более высокий, творческий уровень. Всех с праздником!