3 ms·

> Self referential consistency makes sure I do not make errors within the logical model I have set for myself. It does not help me build better models but once

> Self referential consistency makes sure I do not make errors within the logical model I have set for myself. It does not help me build better models but once those models are built it helps me to compose programs that do not break the invariants in the chosen formalism. I think this is a valid point. But I am less convinced about the second part. I feel that better type systems do help one model the world better (while retaining the consistency checking that you mentioned). In my mind at least having more/better "type tools" is like having differently shaped pieces in your lego tool box. You can create better models for yourself, because the pieces allow you to. And the more experience you have with them, your modeling abilities also improve.

fsloth 12y ago
The Lego analogy is what I also often like to use :) ! " I feel that better type systems do help one model the world better" I agree. But then again, I prefer to start from scribbling mathematical proof mimicking pseudocode which is easily transferred then to statical types. Some people just bang something together, prototype on the IDE/REPL as they go on and they can probably finish faster than me and produce value. If this figure-this-out-while-coding person then has the craftmanship to clean up the code the result is often as good as with the paper-and-pen-first approach. For larger systems, however, I would claim that starting from careful design pays off more because the code-prototype can quickly get out of hands if there are too many abstractions and variables flying in the air at the same time. The 'formal' approach has pitfalls if applied without taste or experience, since, well, modeling for modelings sake can get out of hands at which point one has a shaking tower of abstraction generated from mental masturbation rather than anything of lasting value. This becomes pathological the minute it reaches production. I think we recognize it all has to do with the experience of the programmer and the dedication but craftmanship is very hard to formalize...

fsloth 12y ago

The Lego analogy is what I also often like to use :) ! " I feel that better type systems do help one model the world better" I agree. But then again, I prefer to start from scribbling mathematical proof mimicking pseudocode which is easily transferred then to statical types. Some people just bang something together, prototype on the IDE/REPL as they go on and they can probably finish faster than me and produce value. If this figure-this-out-while-coding person then has the craftmanship to clean up the code the result is often as good as with the paper-and-pen-first approach. For larger systems, however, I would claim that starting from careful design pays off more because the code-prototype can quickly get out of hands if there are too many abstractions and variables flying in the air at the same time. The 'formal' approach has pitfalls if applied without taste or experience, since, well, modeling for modelings sake can get out of hands at which point one has a shaking tower of abstraction generated from mental masturbation rather than anything of lasting value. This becomes pathological the minute it reaches production. I think we recognize it all has to do with the experience of the programmer and the dedication but craftmanship is very hard to formalize...