Hacker News new | past | comments | ask | show | jobs | submit login

> Writing declarative proofs with the machine bridging the intermediate steps is the obvious future.

Do you have a take on what systems are best for this? I found Isabelle/HOL quite reasonable in this respect. There are some toy add-ons to Coq, but I don't think any of them work. There's also FStar which has Z3 integration (if I recall correctly), but last time I played with it it needed quite a lot of hand-holding.

Yes, Isabelle is the best system for this style of proving right now.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact