Hacker News new | ask | show | jobs
by Tainnor 357 days ago
A language without dependent types wouldn't even let you write down the statement of the theorem, so no.