Remix.run Logo
satvikpendem 2 hours ago

It's not about the bugs, it's about designing the layout of the program in types first (ie, laying out all of the data structures required) such that the actual coding of the functionality is fairly trivial. This is known as type driven development: https://blog.ploeh.dk/2015/08/10/type-driven-development/

slowking2 27 minutes ago | parent [-]

At work, I find type hints useful as basically enforced documentation and as a weak sort of test, but few type systems offer decent basic support for the sort of things you would need to do type driven programming in scientific/numerical work. Things like making sure matrices have compatible dimensions, handling units, and constraining the range of a numerical variable would be a solid minimum.

I've read that F# has units, Ada and Pascal have ranges as types (my understanding is these are runtime enforced mostly), Rust will land const generics that might be useful for matrix type stuff some time soon. Does any language support all 3 of these things well together? Do you basically need fully dependent types for this?

Obviously, with discipline you can work to enforce all these things at runtime, but I'd like it if there was a language that made all 3 of these things straightforward.