|
|
|
|
|
|
by garethrowlands
1823 days ago
|
|
|
I don't think types are a red herring here. Because if you follow this advice, then just using logic and your source code, you can prove what data is valid. And, since types and (constructive) logic are so strongly related, then the types are, in some sense "there" even if you don't see them. To put it another way, it's nice if your computer can make the proofs but if it can't, does that make the theorems any less true? |
|
|