3 ms·
Generally, the computer will assist you in this endeavor Kinda. Let's be honest: in production this often turns into a pain in the ass. There's some value in d
by Locke1689 13y ago
Generally, the computer will assist you in this endeavor
Kinda. Let's be honest: in production this often turns into a pain in the ass. There's some value in dependent typing, but providing evidence that concatenating UTF-8 strings is associative is not one of them.
- chrismonsanto 13y agoI have faith that this will get better. We need standard libraries of proofs just as much as we need standard libraries of code. I know Coq has made progress on this, but it's still early days. I do agree with you that there are times when 'full' type checking is inappropriate. Typing is a spectrum, and it's a bit of an art to decide how detailed of guarantees to give for your API.
- bootily 13y agoThat is hilarious. And I also hope your joking.
- chrismonsanto 13y agoThat user is not joking, but note that you generally prove that string concatenation is associative once, not every time.