Jan. 3rd, 2017

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

July 2017

S M T W T F S
      1
23 45678
9101112 13 1415
1617 1819 20 2122
23242526272829
3031     

Most Popular Tags

Page Summary

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 23rd, 2017 02:43 am
Powered by Dreamwidth Studios