Nice Input Shame About The Output

[pigworker]

We now have reached the stage of having a Main.hs file which can be compiled (in the src directory) by

ghc --make Main -o ask

yielding a shell-activated transducer, and the corresponding test file

./ask < ../eg/Proofs.ask

(which contains commutativity of conjunction and also the law of the excluded middle) is successfully mutated into a pile of steaming abstract syntax.

The best way to see if you like it is to check

• grep Junk which will tell you whether any present subproofs have been rejected
• grep Need which will tell you whether any missing subproofs are being demanded

Clearly, this mode of interaction falls short of an accceptable user experience. Some sort of printing is in order.

[elikoga]

While I don't have any deep experience with proof languages and proof assistants I've written a few tiny proofs with coq and have been fascinated by it so I'm intrigued by this project.

I would very much like to contribute to this.

What additions to reach an acceptable mode of interaction are needed?

[pigworker]

Thanks for getting in touch!

A crucial piece of context: this project has only just started and it's going to be deployed at our students within the next few days. Correspondingly, I'm working very hard on this issue already. I have spent today building the machinery for rendering as text the machine's revised version of the user's proof attempt: junk gets commented out; "forgotten" subgoals get inserted as stubs. I think we're nearly at not too bad.

I should have made it clear that this issue was (a) a backhanded celebration of anything working at all and (b) assigned to me already.

But there is plenty still to do. We shall shortly be escaping from propositional logic and beginning to program.

We're building a new proof assistant to give specific support to a new undergraduate course that starts next week. I'll have my work cut out to eliminate false negatives by recognizing everything that's supposed to make sense. Explaining true negatives is more laborious and lower priority: subproofs that don't make sense get commented out, but there should be some reasonable explanation as to why. I'll always be grateful for anyone who can grok what's going on and improve on my sketchy placeholder code.

And yes, it is utterly idiotic to be hacking like hell this close to the wire.

[pigworker]

Two good things have happened today.

Firstly, when a proof is accepted, the user's rendering of the proof should be returned to them.

Secondly, there should be enough of a prettyprinter that machine-generated subgoals are not awful.

That's not deal done by any means, but as it were, now we're talking.