3 ms·
It depends. In the most general case, you have to prove that the program you have given has the type you have asserted. This is similar to proving a mathematica
by chrismonsanto 13y ago
It depends. In the most general case, you have to prove that the program you have given has the type you have asserted. This is similar to proving a mathematical theorem. Generally, the computer will assist you in this endeavor--for example, if you want to prove that A implies B, and A and B are linear inequalities, this can be solved automatically.
- Locke1689 13y agoGenerally, 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.