5 ms·
Have you thought an interactive site where people could learn coq writing proofs? Something very similar to https://projecteuler.net/ https://projecteuler.net/.
by antupis 7y ago
Have you thought an interactive site where people could learn coq writing proofs? Something very similar to https://projecteuler.net/ https://projecteuler.net/. You could get thousands of failed proofs very fast.
- tlringer 7y agoThat's a neat idea. It would mostly help for gathering data from beginners, which would be very skewed, but I'm sure it could still be useful, especially for developing tools to help beginners.
- antupis 7y agoYeah skewing would be definitely problematic, it might be better if it would be similar to Kaggle where people would compete with each other.
- kaiwen1 7y agoThis is a great idea. As I interested novice I'd certainly be a early adopter.