Oleksandr Nikitin (wizzard0) wrote,
Oleksandr Nikitin
wizzard0

Exe/Om presentation in Cloudozer HQ

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

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


Фото © wizzard0

Subscribe
  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 0 comments