3 ms·
It adds to the technical debt of the project. Some teams may never decide they're "ready" for a more sophisticated type system. That's fine, but they're still o
by chongli 7y ago
It adds to the technical debt of the project. Some teams may never decide they're "ready" for a more sophisticated type system. That's fine, but they're still on the hook for maintaining those test suites which might pose significant roadblocks to refactoring or rewriting parts of the system.
- iso-8859-1 7y agoYou can prove a merge sort correct with dependent types. However, a typed implementation of merge sort will arguably be more difficult to mold into a TimSort if it isn't dependently typed. What you say?
- chongli 7y agoI don't have any experience with dependently typed languages. I hope (schedule permitting) to take a course in dependently typed programming (using Agda) and formal verification in the fall. I'll have much more to say on the topic after completing the course.