4 ms·
A better example would be sorting. Most of the time we don't care about how numbers are sorted, we only care about the result. In this hypothetical new language
by akomtu 5y ago
A better example would be sorting. Most of the time we don't care about how numbers are sorted, we only care about the result. In this hypothetical new language, sorting would look like "input: A1..An. output: for all k, Ak < Ak+1." It's implied somewhere in the constraints of the upper function that it'a a permutation, but if you want to be pedantic, you can add "for all k exists m such that Bk=Am."
- valenterry 5y agoYou are making things more complicated than they currently are. Currently I call "list.sorted" and I get a sorted list. What you propose is essentially what some languages like Idris already offer: general purpose programming with constraints that allow the compiler to generate an implementation, given that the constraints are precise enough.