3 ms·
> so why can't we have a programming language that gives you a full blown logic system Most dependently typed programming languages, including Coq, give you t
by curryhoward 9y ago
> so why can't we have a programming language that gives you a full blown logic system
Most dependently typed programming languages, including Coq, give you the ability to basically "do logic" in a mostly unrestricted way.
There are a few challenges that come to mind with making a practical programming language that can also do arbitrary math:
a) For the language to be useful for proving things, it needs to be strongly normalizing. That means all programs halt—otherwise, you could trivially prove any proposition. Unfortunately that limits its utility as a general purpose programming language.
b) The languages which attempt to be useful for theorem proving are generally pure functional languages (due to the strong correspondence between functional programming and logic). Most programmers don't like working in pure functional languages, although the success of Haskell shows that there are certainly programmers who do (myself included).
c) The more expressive a type system is, the more difficult type inference becomes. Yet, paradoxically, I find myself writing more types in languages like C++ and Java than I do in equivalent Coq programs. I believe Coq uses a variant of a bidirectional type inference engine, which is quite usable in practice.
Idris is an attempt to make a practical programming language with the full power of dependent types. So it's probably the closest real language to what you're describing.
Z3 and other SAT/SMT solvers take a different approach: they try to search for proofs automatically, and for certain kinds of math they are very successful. But these are generally only for first-order theories or other restricted kinds of propositions, and not great for general theorem proving. They are good for things like proving array accesses are within bounds, or that you never try to pop from an empty stack (at least that's my understanding of their capabilities).
- iamrecursion 9y agoI should add that something like FStar [0] combines the capabilities of automated theorem proving and a more manual-proof-based dependent type system like that in Idris. It doesn’t have some of the power of Idris’ elaborator reflection, for example, but it can eliminate many long-winded manual proofs via the SMT solver. [0] https://www.fstar-lang.org/ https://www.fstar-lang.org/
- Kutta 9y ago> The more expressive a type system is, the more difficult type inference becomes. This is always mentioned and I always fail to see the relevance. Inferable terms stay inferable when we add dependent types.
- curryhoward 9y ago> I believe Coq uses a variant of a bidirectional type inference engine, which is quite usable in practice. Edit (too late to edit the original comment): After thinking about the kinds of type errors I've seen in my proofs, I think Coq's inference algorithm is based on unification (not bidirectional?). Whatever it is, it's quite nice to work with in any case.
- mietek 9y ago> For the language to be useful for proving things, it needs to be strongly normalizing. That means all programs halt—otherwise, you could trivially prove any proposition. Unfortunately that limits its utility as a general purpose programming language. It’s not true that a strongly normalising language must be limited in utility. See section 4 on codata of Turner’s 2004 “Total functional programmming” for more information. https://github.com/mietek/total-functional-programming/blob/master/doc/pdf/turner-2004.pdf https://github.com/mietek/total-functional-programming/blob/...