4 ms·
And here I thought ADT almost always meant "algebraic data type." Regardless, Rich Hickey's last talk (last month at Clojure Conj) offered a counter argument,
by hellofunk 9y ago
And here I thought ADT almost always meant "algebraic data type."
Regardless, Rich Hickey's last talk (last month at Clojure Conj) offered a counter argument, why ADTs are usually not the best way to organize software (as part of his larger discussion against static typing).
- catnaroek 9y ago> And here I thought ADT almost always meant "algebraic data type." It depends on context > why ADTs are usually not the best way to organize software He clearly hasn't proven anything about his code.
- mike706574 9y ago> He clearly hasn't proven anything about his code. Is that a bad thing? It seems like many people are able to write software that works well and gets the job done without "proving anything" about their code in the way you're describing. Personally, I'm fine with not proving anything if I can deliver quickly and everything works, but I'd like to be convinced otherwise if there's real value there.
- catnaroek 9y agoFor basic infrastructure such as compilers and standard libraries (at least of data structures and algorithms), not providing proofs of correctness is outright criminal.
- blain_the_train 9y agoIt's not though is it... You know, because there aren't actual laws about it. Let's try not to make inflammatory statements.
- lprefontaine 9y agoFormal verification of code has been the elusive Graal seeked by many for now a few decades. It’s a mirage to which many have succumb but like in the desert most died of thirst trying to catch it.