←back to thread

Alan Kay has agreed to do an AMA today

1401 points alankay | 1 comments | 20 Jun 16 18:04 UTC | HN request time: 0.261s | source

This request originated via recent discussions on HN, and the forming of HARC! at YC Research. I'll be around for most of the day today (though the early evening).
1. auggierose ◴[20 Jun 16 19:04 UTC] No.11940426[source]▶
Hi Alan,

what do you think about interactive theorem proving (ITP)? Assuming that you are aware of it, is it something that you have tried? If yes, how was your experience, and which system did you try? If no, why not? What do you think about ITP's role in the grander scheme of things?