Python *

Вышел Python 3.13. Что в этом для не знакомых с Python?

Куй железо не отходя от кассы

Иными словами, Вы тут же захотите его попробовать - самое время, это стало (много) приятнее чем когда-либо.

Что делать и кто виноват

Виноват, очевидно, Гугол - запоздал с увольнениями в команде Python. А делать придётся компиляцию из сорцов - даже в AUR сейчас RC1. Как - на примере Arch в форме EndeavourOS.

Python часть системы, но он 12, поэтому 13 нужно держать отдельно. Скачав с python.org и распаковав

./configure --enable-optimizations --with-lto --enable-experimental-jit=yes --prefix=/home/andy/.python
make

Конечно, чего-то да не хватит, но об этом будет чётко сказано, поэтому и например

yay clang
yay llvm
make

Будет чётко сказано чего не получилось, за 12 такого не помню, у меня - без tkinter. Ну и ладненько. Поскольку make test придумали трусы,

make install
~/.python/bin/python3 -m venv Python13Env
cd Python13Env
python

И наслаждаемся новыми фишками - редактируем процедуры и выходим легко, как по мне - самое очевидное. И да, на первом же (дурацком) тесте - на 10% быстрее.

Каково ваше мнение о https://proofcheck.org? Это cmd-инструмент, который позволяет проверять TEX-овые доказательства на математическую (!) корректность. Но на русском статей о нём нет, хотя он прост в использовании и по своему принципу функционирования. Прилагаю также proof-of-concept от авторов: https://tug.org/TUGboat/tb30-2/tb95neveln.pdf

Суть в том, что до этого существовало много proof assistant-ов, но эти предложили принципиально новый стандарт парсинга логики, который уложился в скрипт на питоне. В отличие от семейства HOL, основные идеи которого восходят аж к 1970-м. Я считаю, что нужно популяризировать ProofCheck и в рунете.