+ DependoBuf, Twelf projects

docs/projects/dependobuf.md

@@ -5,3 +5,32 @@ tags:
 ---
 
 # Протокол для сериализации структурированных данных с зависимыми типами
+
+## Описание
+
+[DependoBuf](https://github.com/SphericalPotatoInVacuum/DependoBuf) —
+очередной протокол для сериализации структурированных данных. Однако в отличие
+от [ProtoBuf](https://protobuf.dev) и иже подобным, наш протокол позволяет
+описание более сложных структур данных: сбалансированных деревьев, массивов
+фиксированной длины, матриц, особым образом провалидированных данных...
+
+Всё это возможно благодаря особенной системе типов, включающей в себя зависимые
+типы таким образом, чтобы сохранять разрешимость проверки типов (т.е. в отличие
+от C++, для DependoBuf существует алгоритм, за конечное время проверяющий
+корректность составленной программы).
+
+В ходе предшествующей работы над проектом, в DependoBuf была реализована
+собственно процедура проверки типов, протокол (де)сериализации в/из байтовых
+последовательностей, а также кодогенерация в различные мейнстримные языки
+программирования.
+
+В этом году предлагается завершить основной этап работы над проектом,
+
+1. убедившись в совместимости различных алгоритмов кодогенерации;
+2. переписав проект с C++ на Rust;
+3. дописав в кодогенерации методы для (де)сериализации типов данных.
+
+## База данных для типов данных DependoBuf
+
+Кроме этого, интересной задачкой является реализация базы данных, поддерживающей
+хранение данных, схема которых описана в протоколе.

docs/projects/twelf.md

@@ -5,3 +5,17 @@ tags:
 ---
 
 # Языковой сервер для Twelf
+
+[Twelf](https://twelf.org) — крайне интересный язык программирования,
+особенный тем, что в нём есть зависимые типы (типы, зависящие от значений),
+но нет правил редукции (вычисления термов). Получается крайне интересная
+система, в которой, помимо всего прочего, легко кодировать грамматики языков
+программирования. Благодаря этому, Twelf часто используется для формализации
+доказательств свойств логических систем (коими языки программирования, конечно
+же, являются).
+
+Однако серьёзным недостатком Twelf является отличие сколько-нибудь комфортного
+тулинга — рекомендуемым способом программирования на Twelf является
+программирование в консоли. В данной дипломной работе предлагается исправить
+столь зияющий недостаток и реализовать языковой сервер (и плагин для VS Code)
+для Twelf для упрощения разработки на нём.

mkdocs.yml

@@ -5,18 +5,18 @@ nav:
   - Главная: index.md
   - Проекты:
     - projects/index.md
-    - projects/catcomp.md
+    - projects/sanskrit.md
+    - projects/zksnark.md
     - projects/codeaswiki.md
     - projects/dependobuf.md
+    - projects/twelf.md
+    - projects/catcomp.md
     - projects/gc.md
     - projects/graphcat.md
     - projects/hitgc.md
     - projects/mlgc.md
     - projects/parsergen.md
-    - projects/sanskrit.md
     - projects/shaderdsl.md
-    - projects/twelf.md
-    - projects/zksnark.md
   - testtask.md
 theme:
   name: material