Source

Agda-LLVM /

Filename Size Date modified Message
Examples
LLVM
30 B
867 B
2.0 KB

Про что это

Общая идея относится к тому, что такое программирование в принципе. Хороший язык программирования позволяет переставлять конструкции и рассуждать об их типах. Хороший программист понимает основные концепции организации кода, алгоритмы и структуры данных.

Пример - C++ template metaprogramming. Проблемы с ним - очень примитивный язык template ов. Нехватка выразительности. Слабые типы. Что делать: взять хороший, выразительный язык. Возьмем agda. Возьмем подмножество LLVM в качестве «целевой платформы», чтобы получать «реальные вещи». На Agda реализуем несколько eDSL.

Приложения

Мне интересно то, что происходит на работе (dataflow системы в тренажерах). Очень интересны микроконтроллеры типа STM32. Они содержат огромное количество аппаратных средств на кристале, которые могут соединяться в графы и работать вообще независимо от процессора.

«Программировать» такие вещи - абсурд. В коде отсутствует модель. Поэтому интересно было бы построить модель на нормальном, выразительном языке, а затем сериями трансформаций получать код.

Ожидаемый результат

Пока это песочница. Постепенно, надеюсь, получится библиотека.