Whenever I do leetcode, I use python. This is because most of the constraints that are useful to check in an algorithm can't be encoded as types. Instead I spri

Whenever I do leetcode, I use python. This is because most of the constraints that are useful to check in an algorithm can't be encoded as types. Instead I sprinkle a lot of asserts (possibly using slower bruteforce version of the code) to check invariants and properties that I expect to be true. I think dependent types is supposed to solve this problem (for example, rather than just a list of ints, it can encode that it's currently a sorted list of ints) but they don't seem practical to use at the moment.