3 ms·
What would need to exist to make such a proof specification utility less boring? I know many engineers who never thought they'd use unit tests until I was able
by gravypod 7y ago
What would need to exist to make such a proof specification utility less boring? I know many engineers who never thought they'd use unit tests until I was able to demonstrate immediate workflow benefit that made their job far easier than before. If you have experience in higher math, what would need to exist to make such specification useful?
- QuesnayJr 7y agoThe challenge is making a tool that's sufficiently ergonomic. It's the UI problem from hell. The problem is that people are much smarter than computers, so you can just specify the broad strokes and your audience can fill in the details as needed.
- Jweb_Guru 7y agoFor starters, it would be nice to be able to make trivial manipulations of algebraic expressions involving real numbers not incredibly tedious. As far as I know no existing proof assistant is up to that challenge. Again, it's not a matter of power--many, many proof assistants can formalize the vast majority of mathematics--it's about UX.