Previous Entry Share Next Entry
photo25

Exe/Om presentation in Cloudozer HQ

Оригинал взят у maxim в Exe/Om presentation in Cloudozer HQ
Протокол заседаний:

1. В нормальные формы рекурсивных типов верится с трудом, для неподготовленного слушателя
2. Вопрос "зачем писать свой движек" а не писать в Coq + экстрактор можно записывать в FAQ
3. Нужно четко разделять доказательства базовой библиотеки, доказательства кодироваки, доказательства существования изоморфизмов между сигнатурами, доказательства корекктности программы. Когда слишком много кванторов и слова "доказательства" мозг у слушателей начинает отключаться. С этим нужно что-то думать.
4. Вопрос о практически прямом преобразовании черч кодировки в FPGA примитивы, популярный.
5. Про сертифицированные C компиляторы все слышали, поэтому это упоминать тоже нужно.
6. Побольше примеров из классического курса математики про брадобреев и отрицание отрицания.


Фото © wizzard0


?

Log in

No account? Create an account