Провёл собственное исследование по языкам программирования будущего.

В целом, дядька Боб правильно уловил ветер и выдвинул правильные требования к языку программирования для AI:
- гомоиконичность;
- явные типы;
- никаких скрытых потоков управления;
- контракты встроены в язык.

Но это пока просто идея. Не реализовано даже формальной верификации контрактов. Типы явные, но это скорее аннотации, чем Хиндли-Милнер. Нет алгебраических типов с exhaustive matching (хотя tagged unions упомянуты). Нет вывода типов.

Если цель - ИИ как полноценный разработчик, нужен язык, который максимизирует вероятность того, что сгенерированный им код корректен. Это значит: сильная система типов (компилятор ловит ошибки ИИ), простота (меньше галлюцинаций), достаточный объём кода в обучающих данных, и путь к формальной верификации.

Lean 4 - стратегически самый интересный, но практически самый рискованный. Если через 5-7 лет Lean станет практическим языком программирования, выбравшие его сейчас окажутся впереди всех. Но не сегодня.

На сегодняшний день выделяются два языка.

Rust - первый кандидат. Огромный объём обучающих данных, ИИ пишет на нём уверенно. Borrow checker отсекает ошибки с памятью. Система типов ловит логические ошибки. Verus, rocq-of-rust, Aeneas для верификации. Экосистема зрелая. Один минус - сложность языка увеличивает вероятность, что ИИ сгенерирует компилируемый, но неидиоматичный код. Тем не менее, строгость компилятора это компенсирует.

Ownership-модель - это фундамент, на котором можно строить доказательства.

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

OCaml - второй кандидат. Меньше обучающих данных, но язык проще, и паттерны более предсказуемые. Алгебраические типы и exhaustive pattern matching - идеальный формат для ИИ-генерации: он описывает все случаи, компилятор проверяет, что ИИ ничего не пропустил. Gospel (Generic OCaml SPEcification Language) - tool-agnostic язык формальных спецификаций для OCaml.

Именно поэтому OCaml используется в финтехе. Экосистема, правда, уступает Rust.

Вишенка на торте - Camlp5. Это OCaml с Lisp-синтаксисом. Типы, компиляция, всё как в OCaml, но добавлена гомоиконичность. S-выражение - это одновременно и программа, и структура данных, которую можно анализировать, трансформировать, генерировать другой программой. Это не макросы как синтаксический сахар - это фундаментальное свойство: программа может порождать программы так же естественно, как оперировать числами.

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

Дейкстра мечтал об этом полвека назад. Но раньше не было генератора, способного превратить спецификацию в код. Теперь он есть - и узкое место сместилось от написания кода к доказательству его корректности.

Это возвращает нас к тому, с чего начался ML (Робина Милнера) - к языку, созданному для доказательства теорем. Круг замыкается.

Милнер в начале 1970-х в Эдинбурге строил LCF - Logic for Computable Functions - систему для доказательства теорем. Ему нужен был язык, в котором на уровне системы типов невозможно было бы сконструировать невалидное доказательство. Так появился ML - Meta Language.

Пятьдесят лет спустя мы приходим к той же задаче, только с другой стороны. Милнер хотел, чтобы человек писал доказательства, а машина их проверяла. Мы идём к тому, что машина будет писать код, а формальная система - проверять его корректность. Задача та же - гарантия корректности через типы. Только роли поменялись.

ML был создан как язык для мира, где код должен быть доказуемо правильным. Этот мир тогда не наступил, потому что индустрии было важнее "быстро и дёшево", чем "правильно". Но если генерация кода становится бесплатной, а цена ошибки растёт - "правильно" побеждает. И оказывается, что фундамент для этого был заложен полвека назад в Эдинбурге.

Хотелось про дроны, но давайте поговорим про Debian и «not enough space»

Ребята, очень хочется написать что-нибудь ещё про дроны, но увы — я к ним никакого отношения не имею. Ну, кроме как дать транспортную сеть, чтобы видео с них нормально шло.

Летать на них при помощи LTE всё равно не выйдет (да, это снова небольшой камень в сторону тех, кто пытается загнать всех в Чебурнет под предлогом благой цели).

Поэтому сегодня с утра поговорим про другое.

У всех в армии есть сервера или АРМы (это Автоматизированные Рабочие Места) на Linux. У нас почти всегда это Astra Linux (а это по сути Debian), Ubuntu (тоже Debian), чистый Debian, Дионис (CLI там точно такой же, как в Debian) и иногда Numa (ну про неё лучше вообще не говорить).

Короче, связисту в армии как ни крути надо знать пару слов про Debian.

Если с командами ip a и ip r уже почти все разбираются, то вот одна ошибка до сих пор вводит многих в ступор:
«not enough space» — место на диске закончилось под ноль.

И почти всегда виноваты логи. Вот простая и понятная инструкция, как это почистить без интернета, без скачивания пакетов и без лишней нервотрёпки.

1. Сначала смотрим, сколько вообще места осталось:

df -h

2. Ищем, где самое большое пожирание:

du -sh /*

(обычно сразу видно, что /var самый жирный)

3. Заходим в логи:

cd /var/log 
du -sh *

4. Чистим старые логи (самое безопасное):

- Для journald (Astra/Ubuntu/Debian):

sudo journalctl --vacuum-time=10d  

(оставит логи только за последние 10 дней) или

sudo journalctl --vacuum-size=500M

(оставит только 500 МБ логов)

- Старые текстовые логи можно просто удалить:

sudo rm -f *.log.*
sudo rm -f *.gz

5. Чтобы в будущем не повторялось, ставим автоочистку:
Открываем файл:

sudo nano /etc/systemd/journald.conf

Находим и меняем строки:

SystemMaxUse=500M SystemMaxFileSize=50M RuntimeMaxUse=200M

Сохраняем (Ctrl+O, Enter, Ctrl+X) и перезапускаем:

sudo systemctl restart systemd-journald

Готово. Место появилось, сервер вздохнул свободно.

Если у кого-то после этих команд что-то пошло не так — пишите в комментариях, разберём.

Communicatio est victoria.

— Душнила @zas_svo
#СВО #связь #Linux #Debian #AstraLinux #сервер