reckless intuitions of an epistemic hygienist (![[info]](http://l-stat.livejournal.com/img/userinfo.gif){kind=small} gustavolacerda) wrote,@ 2006-04-27 00:29:00 |
|
| Entry tags: | formal_ed, programming |
programming & proving simultaneously
from here
Athena is a programming language and an interactive theorem proving environment rolled in one.
Can anyone explain this to me?
--
I occasionally write a function multiple times, in parallel. I wish my language could somehow prove that they are equivalent. What would be the point?, you may ask...
Well, you know how they say programs are meant to read, and only occasionally executed?
Likewise, the goal of a piece of code may be to make a reader understand something.
As any educator knows, redundancy makes learning more robust: the more ways you present something, the better, especially if you can make the student understand why the two presentations are equivalent.
