4 ms·

Theorem proving and complex types are like extensions on an otherwise ordinary language: - Agda, Idris, etc. are functional languages extended with complex typ

Theorem proving and complex types are like extensions on an otherwise ordinary language: - Agda, Idris, etc. are functional languages extended with complex types - Isabelle, Lean, etc. are functional languages extended with complex types and unreadable interactive proofs - Dafny etc. are imperative languages extended with theorems and hints - ACL2 is a LISP with theorems and hints Related, typeclasses are effectively logic programming on an otherwise functional/imperative language (like traits in Rust, mentioned in https://rustc-dev-guide.rust-lang.org/traits/chalk.html https://rustc-dev-guide.rust-lang.org/traits/chalk.html).

nextaccountic 6mo ago
> Agda, Idris, etc. are functional languages extended with complex types I think they are not. No amount of type level extensions can turn a regular functional language like Haskell into something suitable for theorem proving. Adding dependent types to Haskell, for example, doesn't suffice. To build a theorem prover you need to take away some capability (namely, the ability to do general recursion - the base language must be total and can't be Turing complete), not add new capabilities. In Haskell everything can be "undefined" which means that you can prove everything (even things that are supposed to be false). There's some ways you can recover Turing completeness in theorem provers. You can use effects like in F* (non-termination can be an effect). You can separate terms that can be used in proofs (those must be total) from terms that can only be used in computations (those can be Turing complete), like in Lean. But still, you need the base terms to be total, your logic is done in the fragment that isn't Turing complete, everything else depends on it.
- LeCompteSftware 6mo ago
  This is just wrong, you're being too didactic. Idris specifically lets you implement nontotal functions in the same way that Rust lets you write memory-unsafe code. The idea is you isolate it to the part of the program with effects (including the main loop), which the compiler can't verify anyway, and leave the total formally verified stuff to the business logic. Anything that's marked as total is proven safe, so you only need to worry about a few ugly bits; just like unsafe Rust. Idris absolutely is a general-purpose functional language in the ML family. It is Haskell, but boosted with dependent types.
  - andai 6mo ago
    Random passerby chiming in: so this means you can write "regular" software with this stuff? While reading TFA I thought the theorem stuff deserved its own category, but I guess it's a specialization within an ur-family (several), rather than its own family? It definitely sounds like it deserves its own category of programming language, though. The same way Lojban has ancestry in many natural languages but is very much doing its own thing.
    - nextaccountic 6mo ago
      Yes Idris was meant to write regular code. F* is also meant to write regular code But I think that the theorem prover that excels most at regular code is actually Lean. The reason I think that is because Lean has a growing community, or at least is growing much faster than other similar languages, and for regular code you really need a healthy ecosystem of libraries and stuff. Anyway here an article about Lean as a general purpose language https://kirancodes.me/posts/log-ocaml-to-lean.html https://kirancodes.me/posts/log-ocaml-to-lean.html
      - Hendrikto 6mo ago
        > if you're a developer who wants to exploit the multiplicative factor of a truly flexible and extensible programming language with state of the art features from the cutting-edge of PL research, then maybe give Lean a whirl! Does not sound that appealing to me. Sounds like little consistency and having to learn a new language for every project.
  - nextaccountic 6mo ago
    I mentioned this later > You can separate terms that can be used in proofs (those must be total) from terms that can only be used in computations (those can be Turing complete), like in Lean What I meant is that the part of Idris that lets people prove theorems is the non-total part But, I think you are right. Haskell could go there by adding a keyword to mark total functions, rather than marking nontotal functions like Idris does. It's otherwise very similar languages
- deleted 6mo ago
  [deleted]
- solomonb 6mo ago
  I mean you are kinda right but kinda wrong. To get a proof checker you take a typed lambda calculus and extend it with Pi, Sigma, and Indexed Inductive types while maintaining soundness. Yes haskell's `bottom` breaks soundness, but that doesn't mean you need to take away some capability from the language. You just need to extend the language with a totality checker for the new proof fragment.
- User23 6mo ago
  > To build a theorem prover you need to take away some capability (namely, the ability to do general recursion - the base language must be total and can't be Turing complete), not add new capabilities. In Haskell everything can be "undefined" which means that you can prove everything (even things that are supposed to be false). Despite what the fanatical constructivists (as opposed to the ones who simply think it's pragmatically nice) seem to want us to think, it turns out that you can prove interesting things with LEM (AKA call/cc) and classical logic.
  - ChadNauseam 6mo ago
    How does this disagree with "the base language must be total and can't be Turing complete"

nextaccountic 6mo ago

> Agda, Idris, etc. are functional languages extended with complex types I think they are not. No amount of type level extensions can turn a regular functional language like Haskell into something suitable for theorem proving. Adding dependent types to Haskell, for example, doesn't suffice. To build a theorem prover you need to take away some capability (namely, the ability to do general recursion - the base language must be total and can't be Turing complete), not add new capabilities. In Haskell everything can be "undefined" which means that you can prove everything (even things that are supposed to be false). There's some ways you can recover Turing completeness in theorem provers. You can use effects like in F* (non-termination can be an effect). You can separate terms that can be used in proofs (those must be total) from terms that can only be used in computations (those can be Turing complete), like in Lean. But still, you need the base terms to be total, your logic is done in the fragment that isn't Turing complete, everything else depends on it.

LeCompteSftware 6mo ago
This is just wrong, you're being too didactic. Idris specifically lets you implement nontotal functions in the same way that Rust lets you write memory-unsafe code. The idea is you isolate it to the part of the program with effects (including the main loop), which the compiler can't verify anyway, and leave the total formally verified stuff to the business logic. Anything that's marked as total is proven safe, so you only need to worry about a few ugly bits; just like unsafe Rust. Idris absolutely is a general-purpose functional language in the ML family. It is Haskell, but boosted with dependent types.
- andai 6mo ago
  Random passerby chiming in: so this means you can write "regular" software with this stuff? While reading TFA I thought the theorem stuff deserved its own category, but I guess it's a specialization within an ur-family (several), rather than its own family? It definitely sounds like it deserves its own category of programming language, though. The same way Lojban has ancestry in many natural languages but is very much doing its own thing.
  - nextaccountic 6mo ago
    Yes Idris was meant to write regular code. F* is also meant to write regular code But I think that the theorem prover that excels most at regular code is actually Lean. The reason I think that is because Lean has a growing community, or at least is growing much faster than other similar languages, and for regular code you really need a healthy ecosystem of libraries and stuff. Anyway here an article about Lean as a general purpose language https://kirancodes.me/posts/log-ocaml-to-lean.html https://kirancodes.me/posts/log-ocaml-to-lean.html
    - Hendrikto 6mo ago
      > if you're a developer who wants to exploit the multiplicative factor of a truly flexible and extensible programming language with state of the art features from the cutting-edge of PL research, then maybe give Lean a whirl! Does not sound that appealing to me. Sounds like little consistency and having to learn a new language for every project.
- nextaccountic 6mo ago
  I mentioned this later > You can separate terms that can be used in proofs (those must be total) from terms that can only be used in computations (those can be Turing complete), like in Lean What I meant is that the part of Idris that lets people prove theorems is the non-total part But, I think you are right. Haskell could go there by adding a keyword to mark total functions, rather than marking nontotal functions like Idris does. It's otherwise very similar languages
deleted 6mo ago
[deleted]
solomonb 6mo ago
I mean you are kinda right but kinda wrong. To get a proof checker you take a typed lambda calculus and extend it with Pi, Sigma, and Indexed Inductive types while maintaining soundness. Yes haskell's `bottom` breaks soundness, but that doesn't mean you need to take away some capability from the language. You just need to extend the language with a totality checker for the new proof fragment.
User23 6mo ago
> To build a theorem prover you need to take away some capability (namely, the ability to do general recursion - the base language must be total and can't be Turing complete), not add new capabilities. In Haskell everything can be "undefined" which means that you can prove everything (even things that are supposed to be false). Despite what the fanatical constructivists (as opposed to the ones who simply think it's pragmatically nice) seem to want us to think, it turns out that you can prove interesting things with LEM (AKA call/cc) and classical logic.
- ChadNauseam 6mo ago
  How does this disagree with "the base language must be total and can't be Turing complete"