Spock: Difference between revisions
No edit summary |
No edit summary |
||
| Line 1: | Line 1: | ||
Spock is an XO activity and pygtk application that implements a simple text editor with | Spock is an XO activity and pygtk application that implements a simple text editor with | ||
an embedded proof verifier. The proof verifier is based on the | an embedded proof verifier. The proof verifier is based on (an older version of) the | ||
[http://sites.google.com/a/ghilbert.org/ghilbert/home Ghilbert] proof language, | [http://sites.google.com/a/ghilbert.org/ghilbert/home Ghilbert] proof language, | ||
with some modest extensions. Ghilbert in turn is inspired by the | with some modest extensions. Ghilbert in turn is inspired by the | ||