Talk:Proof assistant

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)

I think that Proof assistant should focus on the general aspects, and having all of the examples from the same source may distract from that general view. What I would rather expect is the identification of the individual steps (as you have done it already) and then a discussion of different ways to go about them (I suppose that the different tools will have some noteworthy differences), ideally linking to more detailed articles of the Proof General (software) kind. --Daniel Mietchen 22:10, 14 August 2010 (UTC)

I see. However, to this end you need a more knowledgeable author. I am not an expert in these systems; in fact, this is my first attempt to really understand what is achieved for now. I do not intend to learn other projects, since I am already convinced that they are weaker. Anyone is welcome to do better. Boris Tsirelson 06:02, 15 August 2010 (UTC)