4 ms·
I take you example of the broken computation: v1 = v0 * (t1 / t0) - a A smart lint system with a vocabulary for physics programs could know by convention that
by holri 11y ago
I take you example of the broken computation:
v1 = v0 * (t1 / t0) - a
A smart lint system with a vocabulary for physics programs could know by convention that a name t means time and 0 and 1 means index and that in context of time the greater index means a step ahead in time. (At least this is what 90% of humans would assume). So it could infer t1 > t0 and check that at runtime in some debug mode.
Maybe there are valid cases where t1 < t0 but then this naming introduces under guarantee false human interpretations of the source.
The lint system should model and check against the typical human interpretation of names.
This does not detect the above wrong computation but it could help find errors without writing a test for every function.
- fsloth 11y agoHmm. Isn't a lint system as you describe just an informal static typing system in this case? And anyway, someone still needs to write the lint system. Adding layers of abstraction does not make the problem go away... Sure, when we have well defined domain logic rules those can be enforced through typing. But I would claim it is really unusual to do greenfield development and start from a really well defined set of domain logic rules formalized as a type system. Usually one discovers those rules as one develops the system, and then encodes those rules in types.