6 ms·

Also see: https://rise4fun.com/fstar/tutorial https://rise4fun.com/fstar/tutorial Even though this sounds like formal verification gobbledygook, there is some

Also see: https://rise4fun.com/fstar/tutorial https://rise4fun.com/fstar/tutorial Even though this sounds like formal verification gobbledygook, there is some information of practical value there. How many JSON validators have you seen in python and javascript? Why can't the static type checkers like mypy and pyright do this for us? The answer is that the type systems of these languages are not sufficiently developed. They can tell you if you're assigning a string to an int, but not if you're assigning 200 to an int whose type allows only numbers in [10, 100]. So one creates a new class with a validate() method, which is completely unnecessary and doesn't protect you against integer overflows elsewhere in the code. F* and OCaml derivatives are our best hope in developing a type system which perform these types of common checks in one integrated framework via refinement types and dependent types. Hopefully, one day that work can hit mainstream languages like python, javascript and whatever ends up being the system programming language of choice replacing C in the coming years.

com2kid 6y ago
> The answer is that the type systems of these languages are not sufficiently developed. They can tell you if you're assigning a string to an int, but not if you're assigning 200 to an int whose type allows only numbers in [10, 100]. I am pretty sure Ada did that in the 80s. :) I get what you are saying, but the example you gave is a pretty trivial one that has been solved (although not implemented very often...) for awhile in more "regular" languages!
- adsharma 6y ago
  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-...
- amw-zero 6y ago
  Ada cannot do this at compile time. Predicates with arbitrary logic like that are checked with runtime assertions. There are limits on which static predicates you can write. F* implements refinement and dependent types, which allow true logic to be computed at _compile_ time.
dragonwriter 6y ago
> How many JSON validators have you seen in python and javascript? Why can't the static type checkers like mypy and pyright do this for us? Because JSON is external data, mypy and pyright operate on Python code. > They can tell you if you're assigning a string to an int, but not if you're assigning 200 to an int whose type allows only numbers in [10, 100]. Mypy can, in fact, do that (via a union of literal types), though the UX is horrible for that specific case and it only handles simple literals, but that's actually enough for JSON semantics. Of course, to validate JSON with it, you'd have to turn the JSON into Python code with type annotations and validate that.
- adsharma 6y ago
  Like you're suggesting, external data can be seen as a variant of literals embedded in code. https://www.python.org/dev/peps/pep-0589/ https://www.python.org/dev/peps/pep-0589/ movie: Movie = {'name': 'Blade Runner', 'year': 1982} It's all possible in theory, but the support in widely used static type checkers is very basic or has bad UX. On the other hand, this is exactly what you need to write secure code.
z3t4 6y ago
Type systems do not thinking for you, you still have to make a type with a range check. So you could just as well write function foo(n) { if(n < 10 || n > 100) throw new Error("Expected n=" + n + " to be between 10 and 100"); return n*2; } And while you are at it you can write an unit test that is tested at compile time or in the editor/IDE. // assert(foo(10),20);
- amw-zero 6y ago
  Try reading the tutorial. F* uses refinement types, which means that logic is checked before the program is executed, at compile time.
- tuvistavie 6y ago
  Runtime safety and compile time safety are not the same thing. Compile time safety is not a silver bullet but it does protect against quite a few classes of errors.
eyelidlessness 6y ago
For what it’s worth, the typescript type system is at or nearly at a point where these kinds of constraints are possible (with the caveat that runtime validation requires extra work or compiler level hackery). When TS 4.1 hit beta, I did a proof of concept validating that a `number` was a non-negative integer, and it works[1]. Many similar or even substantially more complex constraints are possible (I’m exploring type level JSON Schema validation of example values, and I’m not quite there but do I believe it’s possible). I’m sure this kind of thing is child’s play in ML family languages, but it’s really cool to get this level of compile time certainty in a dynamic language. [1]: my proof of concept was using literals without accounting for exponential representations etc, but I have no reason to doubt these are also achievable based on the ways I’ve seen 4.1+ used.
- amw-zero 6y ago
  I think the problem with what F* is doing is that it’s so foreign to most people that they don’t actually understand it. Typescript cannot do what you’re saying at compile time. F* knows _at compile time_ whether or not a value is within a range, and you can get a compiler error _without executing the program_.
  - eyelidlessness 6y ago
    TypeScript can do that. That’s what I was saying.
    - indolering 6y ago
      I'm pretty sure TypeScript 4 didn't add support for dependent types. Please cite your source or include a link to source code : ).
    - amw-zero 6y ago
      Please provide a code example.
      - eyelidlessness 6y ago

com2kid 6y ago

> The answer is that the type systems of these languages are not sufficiently developed. They can tell you if you're assigning a string to an int, but not if you're assigning 200 to an int whose type allows only numbers in [10, 100]. I am pretty sure Ada did that in the 80s. :) I get what you are saying, but the example you gave is a pretty trivial one that has been solved (although not implemented very often...) for awhile in more "regular" languages!

adsharma 6y ago
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-...
amw-zero 6y ago
Ada cannot do this at compile time. Predicates with arbitrary logic like that are checked with runtime assertions. There are limits on which static predicates you can write. F* implements refinement and dependent types, which allow true logic to be computed at _compile_ time.

dragonwriter 6y ago

> How many JSON validators have you seen in python and javascript? Why can't the static type checkers like mypy and pyright do this for us? Because JSON is external data, mypy and pyright operate on Python code. > They can tell you if you're assigning a string to an int, but not if you're assigning 200 to an int whose type allows only numbers in [10, 100]. Mypy can, in fact, do that (via a union of literal types), though the UX is horrible for that specific case and it only handles simple literals, but that's actually enough for JSON semantics. Of course, to validate JSON with it, you'd have to turn the JSON into Python code with type annotations and validate that.

adsharma 6y ago
Like you're suggesting, external data can be seen as a variant of literals embedded in code. https://www.python.org/dev/peps/pep-0589/ https://www.python.org/dev/peps/pep-0589/ movie: Movie = {'name': 'Blade Runner', 'year': 1982} It's all possible in theory, but the support in widely used static type checkers is very basic or has bad UX. On the other hand, this is exactly what you need to write secure code.

z3t4 6y ago

Type systems do not thinking for you, you still have to make a type with a range check. So you could just as well write function foo(n) { if(n < 10 || n > 100) throw new Error("Expected n=" + n + " to be between 10 and 100"); return n*2; } And while you are at it you can write an unit test that is tested at compile time or in the editor/IDE. // assert(foo(10),20);

amw-zero 6y ago
Try reading the tutorial. F* uses refinement types, which means that logic is checked before the program is executed, at compile time.
tuvistavie 6y ago
Runtime safety and compile time safety are not the same thing. Compile time safety is not a silver bullet but it does protect against quite a few classes of errors.

eyelidlessness 6y ago

For what it’s worth, the typescript type system is at or nearly at a point where these kinds of constraints are possible (with the caveat that runtime validation requires extra work or compiler level hackery). When TS 4.1 hit beta, I did a proof of concept validating that a `number` was a non-negative integer, and it works[1]. Many similar or even substantially more complex constraints are possible (I’m exploring type level JSON Schema validation of example values, and I’m not quite there but do I believe it’s possible). I’m sure this kind of thing is child’s play in ML family languages, but it’s really cool to get this level of compile time certainty in a dynamic language. [1]: my proof of concept was using literals without accounting for exponential representations etc, but I have no reason to doubt these are also achievable based on the ways I’ve seen 4.1+ used.

amw-zero 6y ago
I think the problem with what F* is doing is that it’s so foreign to most people that they don’t actually understand it. Typescript cannot do what you’re saying at compile time. F* knows _at compile time_ whether or not a value is within a range, and you can get a compiler error _without executing the program_.
- eyelidlessness 6y ago
  TypeScript can do that. That’s what I was saying.
  - indolering 6y ago
    I'm pretty sure TypeScript 4 didn't add support for dependent types. Please cite your source or include a link to source code : ).
  - amw-zero 6y ago
    Please provide a code example.
    - eyelidlessness 6y ago