Я не знаю, какие псевдокоды Вы имеете в виду. Те "псевдокоды" которые я недавно видел (штуки три разных алгоритма) по формальности полностью эквивалентны программному коду. Более того, на языке с юникодом (типа Agda) их можно было бы записать даже короче и понятнее.

Хотя лично мне идея частично-формализованного языка в духе Literate Programming, только лучше, глубоко симпатична.

По слухам, в Color Forth такое было. 😉

Нет, ни разу. colorForth такой же язык программирования в этом плане, как и любой другой.

[чёрт, я когда-то много на Forth писал. До сих пор приятные впечатления!]

"Ни разу" в смысле того, что у Вас в голове, но близко к тому, что у меня. 😊

Датасеты с примерами   переводов псевдокода в код существуют. И модели на них обученные соответственно тоже.

Пока мы смотрели на SysMoLan как всяческие варианты DSL, то всё было плохо и не получалось.

Когда мы сказали, что надо сменить класс языка, сделать его "архитектурным языком", где намеренно relax требование к типизации, то всё у нас резко взлетело. Инструкции типа https://ailev.livejournal.com/1594529.html стали восприниматься как руководство к действию, и у нас немедленно студенты начали выполнять массово работы по моделированию/представлению знаний о важном в их предприятиях. У нас в видеоканале школы много докладов на эти темы от выпускников. Вот только последний из них: https://www.youtube.com/watch?v=0_WycjiSbJg

И это после того, как мы серьёзно рассмотрели рассуждения авторов ArchiMate и аналогичные рассуждения John Sowa о важности "недоопределённости типов" (underspecification) для моделирования.

John Sowa всегда топил одновременно и за строгую логику как представление онтологий, и за underspecification, поэтому его трудно понимать было. Но мы потихоньку разобрались: важное определяется градуально, а не одним махом. Сначала недоспецифицируется, потом самое важное из этого доспецифицируется, потом из этого самое-самое важное формализуется окончательно.

Работы Ванчурина-Вольфа-Кацнельсона-Кунина примерно про то же сейчас, там показывается, в каком месте в эволюции появляется формальность (она неизбежна, типа появления DNA. Ибо цифра нужна не для собственно рассуждения, а для неизменного повторения, защиты от энтропиии чего-то важного. И тут уж разделяется генотип "цифряной" и более аналоговый фенотип, и они меняются на разных масштабах времени. Вот когда мы работаем с ad hoc моделированием чего-то быстроменяющегося в понимании, нам нужны более "аналоговые" переменные, а когда с чем-то уже закосневшим, то железобетонный контроль типов. Текущие "языки" предлагают только один уровень типизации).

Ничего, у нас в планах на эти темы поразбираться в 2022 году. Но понятно, куда копать.

Так я не спорю, что это важно и интересно. Только сразу уточните, что Вас выполнение на компьютере не интересует, или по крайней мере не критично/не сразу. Потому что для тех, кого интересует, никаких вариантов кроме полной формальности просто нет. 🤷‍♀

А если мы забиваем на компы, то тогда вообще возникает вопрос "зачем формализовывать хоть что-то?" Чтобы можно было что? Люди и в неформализованном неплохо разбираются. Большинство -- намного лучше, чем в формализованном, вообще-то.

1. Компьютеры сейчас и с неформальным работают. Те же архитектурные моделеры (они таки не совсем рисовалки). При этом прилагается инструкция, как поделить вычисления по моделированию (включая работу с типами) по мозгам и кремнию.
2. Формализацию и сопутствующую ей логику люди придумали задолго до компьютеров. И нормально так сами вычисляли. Те же доказательства в математике и расчёты в инженерии и физике вполне без компьютеров проводили и сто лет назад тоже.

Мысль о многоуровневой объективации (задание объекта не в один присест, выделение объекта из фона не одним жестом) она не так тривиальна. Что-то типа "нахождение типа методом градиентного спуска от неформального к формальному" )))

звучит как вариация на тему моделчекинга

И ещё вот тут много: https://ailev.livejournal.com/1551283.html

Я где-то видел байку, что на один конкурс в NASA прислали программу на Хаскеле, которую перепутали с псевдокодом.

Это как в анекдоте про армянское радио: "да, только не NASA, а ВМФ США, и не байка, а примечание в статье". 😊

А, это та история с наложением окружностей и самолётами?

Вы только подтверждаете мой тезис: хотим вычислять (хоть на компьютере, хоть на бумажке) -- нужна полная формализация, не хотим -- не нужна.

Но зачем она нужна, если таки не хотим вычислять или это не требуется -- не понятно.

Звучит так, как будто Вы "открыли", что, оказывается, можно не вычислять, и тогда можно не формализовывать! 😉

Если сильно упростить, то да. А так там был какой-то "геосервер". 😁

Я был совершенно уверен, что выступаю именно в этом амплуа. Таки расскажите, где именно это было?

Это мы с вами обсуждали вчера с garbage in => garbage out. 😉