6 ms·

I picked the trivial example on purpose to make the point that none of the top 5 programming languages do it, even if it was solved in the 80s. Recent language

I picked the trivial example on purpose to make the point that none of the top 5 programming languages do it, even if it was solved in the 80s. Recent languages like swift/kotlin (which I expect will see increased usage in coming years) seem to have ignored this area. https://github.com/peter-tomaselli/swift-refined/blob/master/Tests/RefinedTests/RefinedTests.swift https://github.com/peter-tomaselli/swift-refined/blob/master... https://discuss.kotlinlang.org/t/refinement-types/9753/19 https://discuss.kotlinlang.org/t/refinement-types/9753/19

ampdepolymerase 6y ago
Because it requires a non-trivial amount of static analysis work on the compiler side to make the UX comfortable. Rust's borrow checker mechanism took years to become pleasant for the end user to use. There is still next to no adoption of Ada outside of aerospace, defence, and certain embedded programming sectors.
- com2kid 6y ago
  > Because it requires a non-trivial amount of static analysis work on the compiler side to make the UX comfortable. How so? Any modern language that supports operator overloading enables a half arsed version where you create a struct/class for any subtype of integer you want (e.g. `milliseconds`), and then you create binary operators that takes in on both sides your class, and you add bounds checking yourself, and also this way you can restrict allowing "primitive" types from being just added/subtracted willy-nilly. As I ranted about below, a simple "milliseconds" type would make life easier all over the place. Who hasn't mixed up an API call where part of it takes seconds and another part takes milliseconds? That sort of crud should be easy for a simple subtyping system to catch.
  - indolering 6y ago
    So as is the answer to 99 out of 100 questions, it requires a lot of extra time and effort. Getting those guarantees at compile time is very, very, very hard. Even ADA Spark struggles to verify seemingly simple stuff [1, 2]. It is much easier if you trade compile time for runtime verification, which you can do in C# (but not Mono) or via code comments in Java [3]. WRT subtypes: language designers have plenty of motivation to try and push every non-core feature into a library. Programming in Ada kinda sucks because there are soooo many reserved keywords. You are also stuck with bad design decisions forever, like with Java's Date API [4]. Since it's relatively easy to use the newtype pattern to achieve what you want, it probably doesn't factor into the core language design. Which is to say that I largely agree with you, but the people paying for new languages have a different set of priorities. Making a cat video database go faster is very lucrative, but it's only with the rise of cryptocurrencies that there has been significant funding for high-assurance programming languages outside of defense and aerospace. [1]: https://www.imperialviolet.org/2014/09/07/provers.html https://www.imperialviolet.org/2014/09/07/provers.html [2]: https://blog.adacore.com/using-spark-to-prove-255-bit-integer-arithmetic-from-curve25519 https://blog.adacore.com/using-spark-to-prove-255-bit-intege... [3]: https://www.openjml.org/ https://www.openjml.org/ [4]: https://stackoverflow.com/questions/1571265/why-is-the-java-date-api-java-util-date-calendar-such-a-mess https://stackoverflow.com/questions/1571265/why-is-the-java-...
    - com2kid 6y ago
      Thanks for the awesome answer, with citations! As someone who has to do day to day programming in languages with minimal concept of safety (e.g. JavaScript, C), my concern isn't for provably correct, it's for "make my life easier by covering the 90% case." Number of times I've needed to work with 255 bit integers: 0. Number of times I've confused units of time passing into APIs: way too many. Heck on one system I was working on, I had one API that took distance in as thousands of an inch. Everything else was in metric. Fixing that sort of stuff could be done w/o great trouble, and it'd be a huge boon to everyday programmers. Would it be a sexy language feature? No. But it'd make life better.
com2kid 6y ago
It is super annoying that it isn't done more. I'd love to be able to opt in to bounds checking when I feel it is needed. I have no bloody idea why language designers seem so intent on not letting me choose what perf/safety trade-off is worthwhile for me. :/
- pjmlp 6y ago
  Easy, use C++. While not perfect, given its copy-paste compatibility with C, you can opt-in into bounds checking by using the STL data types, or similar. Then you can also make use of compiler switches, to opt-in in changing the behaviour of operator[]() to do bounds checking. With templates, you can opt-in into checked numerics. While not perfect, and maybe it will be replaced by Rust or other candidate someday, it already offered plenty of opt-in possiblities since early 90's, no need to keep writing C.
  - com2kid 6y ago
    > While not perfect, given its copy-paste compatibility with C, you can opt-in into bounds checking by using the STL data types, or similar. I've heard of abuses of templates to add something that resembles proper ranged types, but it is not a path I'd want to go down. Partly, because C++ templates are not an excuse for a proper type system, even if they are a tool that can be used to force a type system into the language. A proper type system lets you do things like add centimeters and meters together, divide by seconds, and pop out a proper unit and ensure no overflow happens. A proper type system lets you easily, without the visual noise or compile time hit that templates have, add bounds checking wherever it is appropriate. type Age is Integer range 0 .. 130 type Day_Of_Week is (Sunday, Monday, Tuesday, Wednesday, Thursday, Friday, Saturday); subtype Working_Day is Day_Of_Week range Monday .. Friday; Take a look at https://en.wikibooks.org/wiki/Ada_Programming/Type_System#Defining_new_types_and_subtypes https://en.wikibooks.org/wiki/Ada_Programming/Type_System#De... For all the flak it gets, Ada did this right long ago. And a huge part of all this is compile time only, and you can opt in/out of the runtime checks as performance dictates. I'd kill for a proper "milliseconds" type everywhere, one that can only have other milliseconds added to it. And then double the fun with a "seconds" type, and a language that keeps track of which is which for me. Why the heck am I writing timeInMs or timeInSeconds still? Subtyping integers should be a basic and primitive operation in any modern language.

ampdepolymerase 6y ago

Because it requires a non-trivial amount of static analysis work on the compiler side to make the UX comfortable. Rust's borrow checker mechanism took years to become pleasant for the end user to use. There is still next to no adoption of Ada outside of aerospace, defence, and certain embedded programming sectors.

com2kid 6y ago
> Because it requires a non-trivial amount of static analysis work on the compiler side to make the UX comfortable. How so? Any modern language that supports operator overloading enables a half arsed version where you create a struct/class for any subtype of integer you want (e.g. `milliseconds`), and then you create binary operators that takes in on both sides your class, and you add bounds checking yourself, and also this way you can restrict allowing "primitive" types from being just added/subtracted willy-nilly. As I ranted about below, a simple "milliseconds" type would make life easier all over the place. Who hasn't mixed up an API call where part of it takes seconds and another part takes milliseconds? That sort of crud should be easy for a simple subtyping system to catch.
- indolering 6y ago
  So as is the answer to 99 out of 100 questions, it requires a lot of extra time and effort. Getting those guarantees at compile time is very, very, very hard. Even ADA Spark struggles to verify seemingly simple stuff [1, 2]. It is much easier if you trade compile time for runtime verification, which you can do in C# (but not Mono) or via code comments in Java [3]. WRT subtypes: language designers have plenty of motivation to try and push every non-core feature into a library. Programming in Ada kinda sucks because there are soooo many reserved keywords. You are also stuck with bad design decisions forever, like with Java's Date API [4]. Since it's relatively easy to use the newtype pattern to achieve what you want, it probably doesn't factor into the core language design. Which is to say that I largely agree with you, but the people paying for new languages have a different set of priorities. Making a cat video database go faster is very lucrative, but it's only with the rise of cryptocurrencies that there has been significant funding for high-assurance programming languages outside of defense and aerospace. [1]: https://www.imperialviolet.org/2014/09/07/provers.html https://www.imperialviolet.org/2014/09/07/provers.html [2]: https://blog.adacore.com/using-spark-to-prove-255-bit-integer-arithmetic-from-curve25519 https://blog.adacore.com/using-spark-to-prove-255-bit-intege... [3]: https://www.openjml.org/ https://www.openjml.org/ [4]: https://stackoverflow.com/questions/1571265/why-is-the-java-date-api-java-util-date-calendar-such-a-mess https://stackoverflow.com/questions/1571265/why-is-the-java-...
  - com2kid 6y ago
    Thanks for the awesome answer, with citations! As someone who has to do day to day programming in languages with minimal concept of safety (e.g. JavaScript, C), my concern isn't for provably correct, it's for "make my life easier by covering the 90% case." Number of times I've needed to work with 255 bit integers: 0. Number of times I've confused units of time passing into APIs: way too many. Heck on one system I was working on, I had one API that took distance in as thousands of an inch. Everything else was in metric. Fixing that sort of stuff could be done w/o great trouble, and it'd be a huge boon to everyday programmers. Would it be a sexy language feature? No. But it'd make life better.

com2kid 6y ago

It is super annoying that it isn't done more. I'd love to be able to opt in to bounds checking when I feel it is needed. I have no bloody idea why language designers seem so intent on not letting me choose what perf/safety trade-off is worthwhile for me. :/

pjmlp 6y ago
Easy, use C++. While not perfect, given its copy-paste compatibility with C, you can opt-in into bounds checking by using the STL data types, or similar. Then you can also make use of compiler switches, to opt-in in changing the behaviour of operator[]() to do bounds checking. With templates, you can opt-in into checked numerics. While not perfect, and maybe it will be replaced by Rust or other candidate someday, it already offered plenty of opt-in possiblities since early 90's, no need to keep writing C.
- com2kid 6y ago
  > While not perfect, given its copy-paste compatibility with C, you can opt-in into bounds checking by using the STL data types, or similar. I've heard of abuses of templates to add something that resembles proper ranged types, but it is not a path I'd want to go down. Partly, because C++ templates are not an excuse for a proper type system, even if they are a tool that can be used to force a type system into the language. A proper type system lets you do things like add centimeters and meters together, divide by seconds, and pop out a proper unit and ensure no overflow happens. A proper type system lets you easily, without the visual noise or compile time hit that templates have, add bounds checking wherever it is appropriate. type Age is Integer range 0 .. 130 type Day_Of_Week is (Sunday, Monday, Tuesday, Wednesday, Thursday, Friday, Saturday); subtype Working_Day is Day_Of_Week range Monday .. Friday; Take a look at https://en.wikibooks.org/wiki/Ada_Programming/Type_System#Defining_new_types_and_subtypes https://en.wikibooks.org/wiki/Ada_Programming/Type_System#De... For all the flak it gets, Ada did this right long ago. And a huge part of all this is compile time only, and you can opt in/out of the runtime checks as performance dictates. I'd kill for a proper "milliseconds" type everywhere, one that can only have other milliseconds added to it. And then double the fun with a "seconds" type, and a language that keeps track of which is which for me. Why the heck am I writing timeInMs or timeInSeconds still? Subtyping integers should be a basic and primitive operation in any modern language.