News for hackers. Stuff that matters.
Re:The future of interactive theorem proving? by fromeroj on Tuesday August 16, 2022 @09:16PM (#32491112)
While this is a very interesting exercise, I see this kind of wild optimism as when the compilers were introduced or "5th generation computer languages" or any other advance in that area, its touted as: "you can just tell the computer what you want in a simple, natural way, and it won't need programmers any longer" while any of those is a significatively improvement, it is very far from the dream.
Re:The future of interactive theorem proving? by fooker on Tuesday August 16, 2022 @10:28PM (#32491607)
>it is very far from the dream.

SQL is the great success story of that generation.

Writing database query and management code in an imperative language is a nightmare.

Re:The future of interactive theorem proving? by LunaSea on Wednesday August 17, 2022 @07:25AM (#32494767)
I don't completely agree. Yes, SQL is a great success but no, the declarativeness was not enough and we end up generating SQL through ORMs, query builders, templating, etc
Re:The future of interactive theorem proving? by fooker on Wednesday August 17, 2022 @09:24PM (#32504072)
I agree that there should have been more innovation on thosd aspects of query languages!

It's a little bit tricky because there aren't much low hanging fruits for academics to write good papers about, so this innovation is up to programmers who want to improve their quality of life when dealing with databases.