4 ms·

ada has some things that rust doesn't. a lot of them (bounded numbers, pre/post conditions) are really good but do not present a case for writing the category o

ada has some things that rust doesn't. a lot of them (bounded numbers, pre/post conditions) are really good but do not present a case for writing the category of program rust targets. nor the other way round, really. when the dust settles and hindley-milner types, rank-n types, substructural types, etc, all complete their respective journeys from "weird thing the academics came up with" to "state of the art in hip new language that managed to compellingly package it" to "fact of life", it is my hope that dependent types will follow suit -- something that bridges the ux gap between theorem prover and general-purpose language where anything from ownership and borrowing to refinement types lives under one HOL umbrella and lets you make just about any guarantee you like. i recommend anyone reading follows the f* project

quag 3y ago
For the curious (as f* is hard to search for): https://fstar-lang.org/ https://fstar-lang.org/
Buttons840 3y ago
One problem with dependant types is having to write the proofs, but perhaps AI can help with this. The type system can be the world the AI lives in, and we don't have to check the proofs too closely, only know that they proved our high level assertions.
- kaba0 3y ago
  I would definitely want a CI pipeline that randomly fails depending on what day ChatGPT has (Yeah, I know about temperature, but AIs are dumb as hell especially at logical inference stuff, so I just went with the comment in a satirical way)
  - Buttons840 3y ago
    You misunderstand. When working with dependent typed languages sometimes you have to prove things. For example, my function might receive a sorted array, but it has to be proved that the array is sorted, otherwise this is a compile time error--remember, all of this is happening at compile time. So, you write the proof using code and check it in with the rest of your code. It's not something that's going to fail randomly, it's just code. If AI wrote the proof, this would be no different than having Copilot fill in some code, it's just code you check into the repo. These proofs often involve writing code, any code, that will pass the type checker. If you can write code, no matter what that code is, and it passes the type checker, the assertion is proved. It's such a well structured problem, "just write code that satisfies these type constraints, any code will do, as long as it type checks", that I think AI might be able to do it quite well. I've commented on this before and it wasn't well received then either. I think most people have never coded in dependently type language and don't appreciate how often you simply want to fill in the holes and connect the dots with any code that type checks. It's been several years since I experimented with dependent types, so I forgot a lot of the details, but I do remember often wanting to just "fill in the gaps", and indeed, there are IDE tools that can often fill in the gaps for you. (Another thing I was surprised to realize about languages with strong type systems is how often there is literally only one possible implementation of a function.)
    - kaba0 3y ago
      I have seen demos of Idris where just the type signature itself allows for automatic function implementation, which is very cool and almost magical. And you are probably right that many of the trivial cases can perhaps be guessed by some AI — but I think in these cases a simple, more deterministic algorithm could also find a match, iterating through a few proving strategies (I believe this is how the aforementioned idris demo worked). What might have resulted in your downvote (I didn’t downvote your comment, I think it adds to the discussion!) is that many people are tired of the over-hype of LLMs, and taken your comment blindly as support of that. With that said, I do think that you overestimate the capabilities of LLMs, as my go to example: they can’t solve even Sudokus. And any other similar, “recursive” thought is simply fundamentally impossible by LLMs in a single step. It is also the barrier in the popularity of dependently types languages - it is easy to give a proof of List::head. Database::connect on the other hand goes through multiple layers of the whole stack, and function proofs do not compose — two trivial to prove functions composition might be impossible to prove, e.g. I can compose 2 such functions and get some unsolved math problem of your choice.
      - Buttons840 3y ago
        LLMs can't solve Sudoku, but neural networks plus tree search can solve Go. As you say, traditional techniques, like a simple tree search can already solve a lot of the "holes" that come up in dependent languages. Perhaps something like AlphaGo combined with a LLM (to accept human guidance using language) could work?
        fragmede 3y ago
        > LLMs can't solve Sudoku Seems like ChatGPT-4 can? And that's not the advanced data analysis model, either. https://chat.openai.com/share/3126e737-3ae5-4f63-996b-b5a768603ec5 https://chat.openai.com/share/3126e737-3ae5-4f63-996b-b5a768...
        Buttons840 3y ago
        I was curious. I generated a very hard Sudoku puzzle and gave it to GPT4, which proceeded to write and execute a Python program to find the solution.
zozbot234 3y ago
Dependent types are actually quite natural in the "compile time evaluated" subset of a programming language like Ada or Rust. For ordinary program code, they run into the obvious issue that dependent typing subverts the usual phase separation between compile and run time, in the absence of an ad-hoc "code extraction" step. Dependent types and contracts also promote "code" to what is effectively the typing level, which introduces thorny API-stability concerns - i.e. the exact way you express a pre/post-condition or invariant in a library API becomes something that downstream users can end up relying on. Apart from that, Rust is already getting there with their advanced const-generics work.

quag 3y ago

For the curious (as f* is hard to search for): https://fstar-lang.org/ https://fstar-lang.org/

Buttons840 3y ago

One problem with dependant types is having to write the proofs, but perhaps AI can help with this. The type system can be the world the AI lives in, and we don't have to check the proofs too closely, only know that they proved our high level assertions.

kaba0 3y ago
I would definitely want a CI pipeline that randomly fails depending on what day ChatGPT has (Yeah, I know about temperature, but AIs are dumb as hell especially at logical inference stuff, so I just went with the comment in a satirical way)
- Buttons840 3y ago
  You misunderstand. When working with dependent typed languages sometimes you have to prove things. For example, my function might receive a sorted array, but it has to be proved that the array is sorted, otherwise this is a compile time error--remember, all of this is happening at compile time. So, you write the proof using code and check it in with the rest of your code. It's not something that's going to fail randomly, it's just code. If AI wrote the proof, this would be no different than having Copilot fill in some code, it's just code you check into the repo. These proofs often involve writing code, any code, that will pass the type checker. If you can write code, no matter what that code is, and it passes the type checker, the assertion is proved. It's such a well structured problem, "just write code that satisfies these type constraints, any code will do, as long as it type checks", that I think AI might be able to do it quite well. I've commented on this before and it wasn't well received then either. I think most people have never coded in dependently type language and don't appreciate how often you simply want to fill in the holes and connect the dots with any code that type checks. It's been several years since I experimented with dependent types, so I forgot a lot of the details, but I do remember often wanting to just "fill in the gaps", and indeed, there are IDE tools that can often fill in the gaps for you. (Another thing I was surprised to realize about languages with strong type systems is how often there is literally only one possible implementation of a function.)
  - kaba0 3y ago
    I have seen demos of Idris where just the type signature itself allows for automatic function implementation, which is very cool and almost magical. And you are probably right that many of the trivial cases can perhaps be guessed by some AI — but I think in these cases a simple, more deterministic algorithm could also find a match, iterating through a few proving strategies (I believe this is how the aforementioned idris demo worked). What might have resulted in your downvote (I didn’t downvote your comment, I think it adds to the discussion!) is that many people are tired of the over-hype of LLMs, and taken your comment blindly as support of that. With that said, I do think that you overestimate the capabilities of LLMs, as my go to example: they can’t solve even Sudokus. And any other similar, “recursive” thought is simply fundamentally impossible by LLMs in a single step. It is also the barrier in the popularity of dependently types languages - it is easy to give a proof of List::head. Database::connect on the other hand goes through multiple layers of the whole stack, and function proofs do not compose — two trivial to prove functions composition might be impossible to prove, e.g. I can compose 2 such functions and get some unsolved math problem of your choice.
    - Buttons840 3y ago
      LLMs can't solve Sudoku, but neural networks plus tree search can solve Go. As you say, traditional techniques, like a simple tree search can already solve a lot of the "holes" that come up in dependent languages. Perhaps something like AlphaGo combined with a LLM (to accept human guidance using language) could work?
      - fragmede 3y ago
        > LLMs can't solve Sudoku Seems like ChatGPT-4 can? And that's not the advanced data analysis model, either. https://chat.openai.com/share/3126e737-3ae5-4f63-996b-b5a768603ec5 https://chat.openai.com/share/3126e737-3ae5-4f63-996b-b5a768...
        Buttons840 3y ago
        I was curious. I generated a very hard Sudoku puzzle and gave it to GPT4, which proceeded to write and execute a Python program to find the solution.

zozbot234 3y ago

Dependent types are actually quite natural in the "compile time evaluated" subset of a programming language like Ada or Rust. For ordinary program code, they run into the obvious issue that dependent typing subverts the usual phase separation between compile and run time, in the absence of an ad-hoc "code extraction" step. Dependent types and contracts also promote "code" to what is effectively the typing level, which introduces thorny API-stability concerns - i.e. the exact way you express a pre/post-condition or invariant in a library API becomes something that downstream users can end up relying on. Apart from that, Rust is already getting there with their advanced const-generics work.