...Ну и наконец приближаемся ко дну и пробиваем его 😁

Последний минимальный приемлемый язык -- C#.
Теперь у нас уже нету паттерн матчинга "из коробки" и алгебраических типов данных, существенно проигрываем F# как математической нотации, но зато в девятке появились record types, source generators, а так же продвинутые дженерики:
bool IsConnected<U>(HomotopyType<U, IPath<U>> other) where U : IComparable<U>
и даже метапрограммирование:
bool IsHomotopic<T>(this T value, Func<T, bool> predicate)

3. C# хз, ну если только с F# по каким-то совсем конкретным нюансам не получится. В коре на F# эндпоинты вообще в пару строк задаются 😊

[<ApiController>]
[<Route("api/[controller]")>]
type ProofController() =
[<HttpPost>]
member _.ProcessProof([<FromBody>] req: ProofRequest) =
let response = {
Status = true
Result = sprintf "Processed: %s" req.Theorem
}

...
let app = WebApplication.Create()
app.MapGet("/dwarf", fun () -> dwarf)
app.MapPost("/dwarf", fun (dwarf: Dwarf) ->
... Results.Created("/dwarf", dwarf))
app.Run()

=

Посадка на дно начинается с "хотт на питончике" )))
Задаём термы (лямды, универсы, pi-) как датаклассы, а динамическая типизация позволяет вытворять разные штуки на уровне F#.

По большому счёту конечно всё это можно сделать интерпретацией чисто на символьном уровне, как я пытался на пыхе, но слишком уж велика трудоёмкость. В принципе, 50% MLTT (лямбда-исчисление, аппликация и зависимые типы) я упаковал где-то в 200 строк PHP-кода 👊
Но дальше, когда полезли в индуктивные типы, универсумы и особенно рекурсивные определения, без какой-то минимально адекватной типизации, с тайп инференсом в чисто символьных вычислениях начинается полный хардкор 🤘

4. MLTT++ на Python по-взрослому (термы/значения как типы данных).

Несомненный плюс питона технический: реализация получается полностью прозрачной и переносимой куда угодно, хоть в браузере запускай
(кстати, lean умеет компилироваться в wasm...).


5. Ну и в заключение пробиваем дно: пыхапы :)
Ничего не могу сказать, с него я начинал - им же и закончу?
Если получится что-то на питоне, то можно в принципе его код достаточно легко конвертнуть в php...

=

HoTT в Lean 4: 3/10 (почти готовая реализация)
HoTT в F#: 8/10 (практически с нуля, но система типов близка к математической нотации)
HoTT в C#: 9/10
HoTT в Python: 10/10
HoTT в PHP: 12/10

=

В общем, буду пробывать в таком порядке:

4. MLTT++ на Python по-взрослому
1. Lean 4 : REST + HoTT
2. F#
3. C#
4. PHP

Успех предрешён и неминуем.