1. ppavel
  2. Agda-LLVM

Commits

Pavel Perikov  committed fd4b3bf Merge

merge

  • Participants
  • Parent commits 3f5acc6, 53f2f37
  • Branches default

Comments (0)

Files changed (1)

File README.md

View file
+# Про что это
+
+Общая идея относится к тому, что такое программирование в принципе. Хороший язык программирования позволяет переставлять конструкции и рассуждать об их типах. Хороший программист понимает основные концепции организации кода, алгоритмы и структуры данных.
+
+Пример - C++ template metaprogramming. Проблемы с ним - очень примитивный язык template ов. Нехватка выразительности. Слабые типы.
+Что делать: взять хороший, выразительный язык. Возьмем agda. Возьмем подмножество LLVM в качестве «целевой платформы», чтобы получать «реальные вещи». На Agda реализуем несколько eDSL.
+
+## Приложения
+
+Мне интересно то, что происходит на работе (dataflow системы в тренажерах).
+Очень интересны микроконтроллеры типа STM32. Они содержат огромное количество аппаратных средств на кристале, которые могут соединяться в графы и работать вообще независимо от процессора.
+
+«Программировать» такие вещи - абсурд. В коде отсутствует модель. Поэтому интересно было бы построить модель на нормальном, выразительном языке, а затем сериями трансформаций получать код.
+
+## Ожидаемый результат
+
+Пока это песочница. Постепенно, надеюсь, получится библиотека.