Talk:Proof assistant

From Citizendium
Revision as of 16:44, 14 August 2010 by imported>Boris Tsirelson (→‎Example session: why not just here?)
Jump to navigation Jump to search
This article is developing and not approved.
Main Article
Discussion
Related Articles  [?]
Bibliography  [?]
External Links  [?]
Citable Version  [?]
 
To learn how to update the categories for this article, see here. To update categories, edit the metadata template.
 Definition A computer program used interactively for developing human-readable reliable mathematical documents in a formal language. [d] [e]
Checklist and Archives
 Workgroup categories Mathematics and Computers [Please add or review categories]
 Talk Archive none  English language variant American English

Example session

I find this section very illuminating but I wonder whether it is properly placed in this article. It could probably go to a subpage here, but why not put it into an article of its own, e.g. Proof General (software)? --Daniel Mietchen 21:33, 14 August 2010 (UTC)

Of course it could be elsewhere, but for now I wonder why not just here. Do you think that it illuminates only Proof General? My intention was to give some (very modest) impression of what all that is about, so that the reader can decide whether he/she wants to know more, or not. And I had in mind a reader not (yet) interested specifically in some part (say, Proof General) but only in the whole. Does it make sense? Boris Tsirelson 21:44, 14 August 2010 (UTC)