Email Gateway (Aug 22 2022 at 19:08): Email Gateway (Aug 22 2022 at 19:08):From: "John F. Hughes" <jfh@cs.brown.edu>
I'm not certain whether this is appropriate for this list, but here goes:
I've been trying to make progress with Isabelle, but evidently need some
guidance; answers i've gotten here have been of some use, but the
turnaround is a bit slow: I'd like to dedicate a couple of solid days to
making progress, rather than 10 minutes, then hit a stumbling block, and
wait a day or two for an answer, which is how things have gone so far.
I'd like to hire someone (a graduate student?) to answer my questions,
perhaps via email, perhaps in a couple of skype sessions, whatever works
best, allowing for time differences, etc. (I'm on the east coast of the
US). If anyone knows of someone who might be willing to help out, I'd sure
appreciate pointers. You could refer such a person to me directly.
Typical questions may range from the mundane ("Q: Why are there no colors
when I type stuff, but all the examples in the book show colored text?"A:
Because you named your file myTest rather than myTest.thy.") to the more
sophisticated ("Q: I'd like to inductively construct an infinite set (where
"sets" for me are being represented by types) and then prove things about
it... how on earth do I do that?") None of my question are likely to be
about the core ideas of Isabelle itself ('how is the current state of known
facts represented?'), at least not initially --- they're all very much from
a user's perspective.
My target is proving things in mathematics, not things about programming
languages or programs. [I find those applications interesting too, but
they're not what I'm after right now.] So someone with a bit of
mathematical sophistication would probably be ideal.
Thanks in advance for any suggestions.
--John
Last updated: Apr 25 2024 at 16:19 UTC