4da 20.04.2012 10:27 darkstar

via comp.lang.lisp:

The Remote Agent Experiment: Debugging Code from 60 Million Miles Away

Recommended by: @dorfe
1. gds 20.04.2012 10:35 umodni1EDB5EED

видео не смотрел, но порицаю: в разные железяки, особенно в подобные, нужно заливать только формально-проверенный код.

2. 4dagds /1 20.04.2012 10:40 darkstar

Полностью формально верифицируемый код на сильном языке может не все. Таким образом, реализацию все равно пришлось бы делать на менее сильном языке, где уже можно допустить ошибки.

3. gds4da /2 20.04.2012 10:46 umodni1EDB5EED

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

4. 4dagds /3 20.04.2012 10:52 darkstar

на каком языке? трансляция agda→haskell плюс дописывание непроверяемых частей?

5. gds4da /4 20.04.2012 10:56 umodni1EDB5EED

это слишком сложно и ненадёжно, как раз из-за непроверяемых частей. Я бы сделал, например, dsl на coq с доказанной трансляцией в машинный код, имеющий заданную семантику, проверенную при изготовлении процессора.

6. 4dagds /5 20.04.2012 11:01 darkstar

хм, в coq же нет бесконечной рекурсии, как вы сделаете простую циклограмму, например?

7. gds4da /6 20.04.2012 11:07 umodni1EDB5EED

зато в dsl бесконечная рекурсия возможна. Далее, например, возможно использовать коиндуктивные типы данных для представления состояния, и через подходы, подобные бисимуляции, доказывать эквивалентность программ до и после компиляции. Ну или как-то ещё сделать — я пока не просифуанал, я только учусь.
Но то, что это возможно — не сомневаюсь, хотя бы из-за существования CompCert (проверенного почти-сишного компилятора).

Do you really want to delete ?