4 ms·

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

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.
      - kaba0 3y ago
        Which is not the same as it solving it, as there are a million sudoku solvers in its training set.
  - Smaug123 3y ago
    You can still make mana on https://manifold.markets/Mira/will-a-prompt-that-enables-gpt4-to https://manifold.markets/Mira/will-a-prompt-that-enables-gpt... if you believe LLMs can't solve Sudoku!

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.
    - kaba0 3y ago
      Which is not the same as it solving it, as there are a million sudoku solvers in its training set.
- Smaug123 3y ago
  You can still make mana on https://manifold.markets/Mira/will-a-prompt-that-enables-gpt4-to https://manifold.markets/Mira/will-a-prompt-that-enables-gpt... if you believe LLMs can't solve Sudoku!