Mario Carneiro wrote:
If there is enough interest from others that I'm not the only one on the project, I don't mind taking the lead here.
I suppose this is the time to express interest or lack of interest. I will express a small amount of interest. In terms of the value of the concept, the interest comes from the idea that I can think of various things (new features, cleaning up various rough edges, fixing buggy or odd behaviors, etc) we might want which aren't in metamath.exe or mmj2 . And that those two codebases - for all their usefulness - are I suspect hitting a bit of a limit in terms of whether you'd want to want to do a lot of new development to them.
I'll also express a small amount of interest in terms of whether I might help (one thing which springs to mind is automated testing - in the context of a verifier especially a testsuite of proofs which should be rejected).
But emphasis on the word "small". My experience trying to work on the software side of systems like JHilbert and ghilbert has been that (a) software development is a lot of work relative to how much hobby time I have for it, (b) it is a lot easier with a critical mass of users, other contributors, etc, and there are few proof systems which get beyond the stage of "one author" or "one author and the students in their lab". For those reasons I have chosen to devote my energy to metamath, because it already has this kind of critical mass and I get to work on mathematics rather than tools.
So you'll need people other than me to satisfy "I'm not the only one". Especially if you are trying to get a thesis done, I'd recommend that you be realistic and set the bar fairly high in terms of how many offers of participation (and real live participation) will be needed to get this even to the "minimally useful at one set of tasks" stage (much less the larger visions of what we want it to be eventually).
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/9402eb8c-4b69-678a-e188-64f9314967e5%40panix.com.
