Jan. 3rd, 2017

jamhed: (Default)
Написал вот первую программу (теорию) на Isabelle/HOL, вида double m = add m m, где double и add определяются рекурсивно. Потрясающе, на самом деле: никаких тебе тестов, свойства доказываются по индукции, что именно из свойств надо доказать система подсказывает автоматически. Proof assistant! Если что-то доказано, то можно больше никогда не беспокоиться что доказанное работает корректно.

September 2017

S M T W T F S
     1 2
3 4 56 78 9
10111213 14 1516
171819 20212223
24252627282930

Most Popular Tags

Page Summary

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 21st, 2017 06:49 am
Powered by Dreamwidth Studios