4 ms·
The purpose of a type system is to allow the programmer to more fully express their intent in a way that allows static analysis to reject code which runs counte
by codebje 8y ago
The purpose of a type system is to allow the programmer to more fully express their intent in a way that allows static analysis to reject code which runs counter to that intent. Not to alter the compiled code.
That there's no difference between a const ptr and a ref at runtime is irrelevant, because there's a significant difference at compile time.
- pjmlp 8y agoIs very much relevant, because it is an uphill battle in C and C++ communities to get certain groups to adopt better type safer abstractions if that isn't the case.
- sgift 8y agoThe one about pointers being the same at runtime tripped me up too. At the end of the day we only have JMP at the assembly level, but we still are happy if we can use while, for and if.
- ivanbakel 8y agoA good type system can affect the compiled code through valuable static analysis, though. Recognising when optimisations are possible via type restrictions or techniques like monomorphising is an important part of modern typed compilers.
- AstralStorm 8y agoI'd prefer stronger methods like logic proofs and constraint or contract specifications. Compilers could use those even better to optimize and check the meaning of the program. Types are very limited logic constraints after all. While at it, you could ditch some of the old language. Ultimately, everything is just some place in memory, cache and/or CPU register.
- icebraining 8y agoDependent types can encode constraints and require proofs.
- AstralStorm 8y agoYes they do. In a supremely roundabout way typically making for ugly fat proofs for anything high order. Sometimes, rarely, they make proofs cleaner and more direct than high order logic. Plus there is the potential undecidability if you want to use automated type deduction. Hard to spot where the types have to be so to speak reified with bad error messages.