7 ms·

I might add another class of languages: those intended to express proofs, via the Curry-Howard correspondence. Lean is a primary example here. This could be

by pfdietz 7mo ago

I might add another class of languages: those intended to express proofs, via the Curry-Howard correspondence. Lean is a primary example here. This could be considered a subclass of functional languages but it might be different enough to warrant a separate class. In particular, the purpose of these programs is to be checked; execution is only secondary.

armchairhacker 7mo ago
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 7mo 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 7mo 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 7mo 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 7mo 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 7mo 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.
LeCompteSftware 7mo ago
Lean is definitely a dependently typed ML-family language like Agda and Idris, so "ML" has it covered. And the long-term goal of Lean certainly is not "execution is only secondary"; Microsoft is clearly interested in writing real software with it: https://lean-lang.org/functional_programming_in_lean/Programming-with-Dependent-Types/Worked-Example___-Typed-Queries/#typed-queries https://lean-lang.org/functional_programming_in_lean/Program... OTOH if you really want to emphasize "intended to express proofs" then surely Prolog has that covered, so Lean can be seen as half ML, half Prolog. From this view, the Curry-Howard correspondence is just an implementation detail about choosing a particular computational approach to logic.
solomonb 7mo ago
These fall directly out of ML.
zozbot234 7mo ago
These are not true programming languages because by definition they are not Turing complete. If they were Turing complete it would be possible to write a false proof that just compiled down to a non-terminating program.
- gf000 7mo ago
  There has never been a requirement for a "true" programming language to be Turing complete. Also, basically every such language has escape hatches similar to unsafe in Rust to allow expressions that are not provably terminating. They can then just be accepted as an axiom.
  - mcmoor 7mo ago
    I feel like Turing completeness has always been set as the boundary of programming language if there's any boundary at all. That's what people has been using to not include HTML as programming language for example. Or to include MTG as one.
    - gf000 7mo ago
      I think it's a pretty recent thing. Turing completeness is neither a sufficient nor a required property. HTML is not a programming language, it's a markup language - it's in the name, and it's the way it is used (it's not used to describe any kind of computation, it's straight up data that is parsed by algorithms). Neither is PowerPoint, or game of life a programming language even though both are Turing complete.
      - pfdietz 7mo ago
        Is Ladder Logic a programming language? It's used to program industrial controllers, and I don't believe it's Turing complete. https://en.wikipedia.org/wiki/Ladder_logic https://en.wikipedia.org/wiki/Ladder_logic
    - codebje 7mo ago
      Turing completeness is the upper bound of computability, not the lower bound. It's useful mostly for showing that some thing can express the full range of computable problems, or for snarking that some thing is far more complex than it has any right to be. Total languages omit partiality and non-termination from Turing completeness. Partiality is IMO irrelevant when it comes to computability. Any partial function (that is, one whose range is not defined over its whole domain) can be expressed as a total function by either constricting the domain or expanding the range. For example, a "pop" operation on a stack is not defined for an empty stack. You can just loop forever if pop() is called on an empty stack. Alternatively, you can require that pop() is given a witness that the stack is non-empty, or you can require that pop() returns either the top-most element of the stack or a value that indicates the stack was empty. Both let you compute the same set of things as the former. Non-termination is required to be Turing complete, because being Turing complete means being able to compute functions that one cannot reasonably expect to complete before the heat death of the universe. In _practice_ every function terminates when the computing process dies due to some external factor: process runs out of memory ("real" Turing machines have infinite memory!), user runs out of patience, machine runs out of power, universe runs out of stars, that sort of thing, so _in practice_ doing 2^64 iterations before giving up will generally* give you the same outcome as doing an unbounded number of iterations: it'll either terminate, or the process will be killed (here, due to reaching its iteration limit). On the flip side, giving up non-termination and partiality only gives you increased correctness. If there's one thing we've definitely established in computing, it's that we will readily discard correctness to gain a little extra productivity. Why make a developer implement code to handle reaching an iteration limit when you can just make the user get sick of waiting and kill your app? * 18 quintillion is a very large number. Have a try. The most trivial recursive function, on my M4 Mac, when convincing clang to be smart enough to turn it into a loop but dumb enough not to elide it altogether, would take a bit shy of 600 years to complete if iterating ULONG_MAX times; I didn't wait for that, if I'm honest with you, I ran it with a much smaller iteration count and multiplied it out.
User23 7mo ago
This is all of them, properly speaking. Incidentally, this is pretty much what Algol 60 was designed for and why to this day many academic papers use it or a closely related pseudocode.

by pfdietz 7mo ago

armchairhacker 7mo ago

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 7mo 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 7mo 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 7mo 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 7mo 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 7mo 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.

LeCompteSftware 7mo ago

Lean is definitely a dependently typed ML-family language like Agda and Idris, so "ML" has it covered. And the long-term goal of Lean certainly is not "execution is only secondary"; Microsoft is clearly interested in writing real software with it: https://lean-lang.org/functional_programming_in_lean/Programming-with-Dependent-Types/Worked-Example___-Typed-Queries/#typed-queries https://lean-lang.org/functional_programming_in_lean/Program... OTOH if you really want to emphasize "intended to express proofs" then surely Prolog has that covered, so Lean can be seen as half ML, half Prolog. From this view, the Curry-Howard correspondence is just an implementation detail about choosing a particular computational approach to logic.

solomonb 7mo ago

These fall directly out of ML.

zozbot234 7mo ago

These are not true programming languages because by definition they are not Turing complete. If they were Turing complete it would be possible to write a false proof that just compiled down to a non-terminating program.

gf000 7mo ago
There has never been a requirement for a "true" programming language to be Turing complete. Also, basically every such language has escape hatches similar to unsafe in Rust to allow expressions that are not provably terminating. They can then just be accepted as an axiom.
- mcmoor 7mo ago
  I feel like Turing completeness has always been set as the boundary of programming language if there's any boundary at all. That's what people has been using to not include HTML as programming language for example. Or to include MTG as one.
  - gf000 7mo ago
    I think it's a pretty recent thing. Turing completeness is neither a sufficient nor a required property. HTML is not a programming language, it's a markup language - it's in the name, and it's the way it is used (it's not used to describe any kind of computation, it's straight up data that is parsed by algorithms). Neither is PowerPoint, or game of life a programming language even though both are Turing complete.
    - pfdietz 7mo ago
      Is Ladder Logic a programming language? It's used to program industrial controllers, and I don't believe it's Turing complete. https://en.wikipedia.org/wiki/Ladder_logic https://en.wikipedia.org/wiki/Ladder_logic
  - codebje 7mo ago
    Turing completeness is the upper bound of computability, not the lower bound. It's useful mostly for showing that some thing can express the full range of computable problems, or for snarking that some thing is far more complex than it has any right to be. Total languages omit partiality and non-termination from Turing completeness. Partiality is IMO irrelevant when it comes to computability. Any partial function (that is, one whose range is not defined over its whole domain) can be expressed as a total function by either constricting the domain or expanding the range. For example, a "pop" operation on a stack is not defined for an empty stack. You can just loop forever if pop() is called on an empty stack. Alternatively, you can require that pop() is given a witness that the stack is non-empty, or you can require that pop() returns either the top-most element of the stack or a value that indicates the stack was empty. Both let you compute the same set of things as the former. Non-termination is required to be Turing complete, because being Turing complete means being able to compute functions that one cannot reasonably expect to complete before the heat death of the universe. In _practice_ every function terminates when the computing process dies due to some external factor: process runs out of memory ("real" Turing machines have infinite memory!), user runs out of patience, machine runs out of power, universe runs out of stars, that sort of thing, so _in practice_ doing 2^64 iterations before giving up will generally* give you the same outcome as doing an unbounded number of iterations: it'll either terminate, or the process will be killed (here, due to reaching its iteration limit). On the flip side, giving up non-termination and partiality only gives you increased correctness. If there's one thing we've definitely established in computing, it's that we will readily discard correctness to gain a little extra productivity. Why make a developer implement code to handle reaching an iteration limit when you can just make the user get sick of waiting and kill your app? * 18 quintillion is a very large number. Have a try. The most trivial recursive function, on my M4 Mac, when convincing clang to be smart enough to turn it into a loop but dumb enough not to elide it altogether, would take a bit shy of 600 years to complete if iterating ULONG_MAX times; I didn't wait for that, if I'm honest with you, I ran it with a much smaller iteration count and multiplied it out.

User23 7mo ago

This is all of them, properly speaking. Incidentally, this is pretty much what Algol 60 was designed for and why to this day many academic papers use it or a closely related pseudocode.