I haven't looked much into this yet -- it seems very neat! -- but I wonder how hard it would be to create some kind of tactic language for this, akin to what the more conventional proof assistants like Coq, HOL, etc. have. If done minimalistically, it shouldn't blow up the project all that much, though ideally the system would be expandable with user-defined tactics. Not sure whether that tactic language would be inside the Formality language itself (like Coq does) or inside some already-existing language that is meta with respect to the Formality language (like HOL does). Having an already established language for that seems more convenient, but I'm not sure.
Not pretending to be an expert but I did a lot of proofs in Agda (a related subject was my bachelor's thesis). In what way do you find tactics useful? I personally find Coq having bunch of mini-languages inside, one being a tactic language confusing. I think it's a non-optimal (though viable) solution to the problem. I think, as always, lisp gets it right. Computing is all about abstractions and sometimes even abstractions that can talk between each other and the best way to approach this problem is homoiconicity. I think agda gets it right, if you write macros helping you solve the problem at hand you can write very elegant and readable proofs. I understand that tactics are very popular in proof automation community and I'm very likely very wrong. But this is just a reflection of my experience. I'm currently writing my own dependently typed PL and am debating merits of tactics. So far I can't find a reason to add them provided you give enough lispness to your language.
Tactics are very useful when developing proofs rather than dependently typed programs (unless you are using very precise types, as is common in e.g. the Coq program package).
The point is that in a proof you are usually not interested in the precise shape or computation behavior of the underlying proof term and this allows you to use far more aggressive automation than what you are doing with a typical macro. Likewise, you don't really want to see the proof term in the first place. Think about how long chains of equational reasoning are encoded in type theory - this is just noise that detracts from writing your proofs.
As for homoiconicity, I think this is orthogonal to a tactic language. Both lean's tactics and template Coq allow you to reify the syntax of the type theory in order to write automation tactics, but this is separate from the proof search aspects of tactics.
My experience with this kind of stuff: done some Coq by myself and some HOL in class.
Generally, the distinguishing feature of tactics is that they provide backward reasoning, instead of forward reasoning, what a verification engine would be written around. Mind that I haven't worked with any proof system yet besides Coq and HOL, so my opinion might be far out, but I think backward reasoning is a very nice way to construct proofs, especially in the context of a proof assistant.
Aren't things like algorithms for simple automated proving more easily embedded in a tactic language than in a forward reasoning language? When reasoning backward, one naturally reduces the statement to prove to simpler and simpler statements, and at some point they become simple enough to be handled by some automatic prover. (auto/omega/... in Coq, PROVE_TAC/COOPER_TAC in HOL) When reasoning forward, I don't see how one would go about using automated provers like that, but it's likely I'm missing some idea here.
> I'm currently writing my own dependently typed PL
Awesome! I'm all for writing interesting new languages and implementations, especially in this area. Once you've got something to show, be sure to post here on HN, since people might enjoy looking around. :) (If it doesn't get lost in the swarm of submissions...)
I think forward reasoning works only because the underlying type theory is intuitive. When I approach proofs in agda, I simply approach it the same way I write haskell code. "You have bunch of cosets and you wanna go to group." You have objects (proofs) around and you want to construct an instance of a type (theorem) so you start with functions (lemmas) that give objects of desired types. Again, I'm not very familiar with Coq (only agda) but I suppose by backwards reasoning you mean the last unconstructed type in your proof is the type with highest level of abstraction. On the other hand, in agda it's the first one because either you already know a function (lemma) returning this type and need to construct it's arguments (assumptions) or you can use an anonymous function (implication introduction).
This is a totally random and not a well-thought-out statement but to me it seems like the difference between agda and Coq seems like the difference between purely functional and imperative programming.
I think I just need to try out something like Agda before I make any more claims :) Does Agda have something that can automatically prove small formulas in e.g. pure predicate logic?
Backwards reasoning works something like this: to prove 'forall n: P n', it is sufficient to prove 'P 0' and 'P n => P (succ n)', so if you have 'forall n: P n' as your so-called proof goal, you can use the induction tactic to transform that into two goals: 'P 0' and 'P n => P (succ n)'. You then have to separately prove both goals. The tactic system then basically build the actual proof by putting everything on a stack and applying in reverse: once you've proved both goals, it knows it can apply the forward-reasoning induction proof function to construct a proof of the original statements from the two proofs you gave.
> the difference between agda and Coq seems like the difference between purely functional and imperative programming.
Bold, bold :) I'll have to try Agda before I can comment on that. Coq proofs do seem a bit inperative, so there's that.
> The tactic system then basically build the actual proof by putting everything on a stack and applying in reverse: once you've proved both goals, it knows it can apply the forward-reasoning induction proof function to construct a proof of the original statements from the two proofs you gave.
In Agda, you would type something like `nat-ind ?x ?y` into a hole of type (forall m -> P m). Then ?x becomes a hole of type (P zero) and ?y becomes a hole of type (forall n -> P n -> P (suc n)), and you can fill these holes with proofs at your own leisure. It does not feel all that different from using `induction m` in Coq. In Agda, you'd normally implement your "reflective tactics" as functions, or you'd write macros if you really need them (e.g. for ring solvers), but there is no separate tactic language and proofs are never tactic scripts.
No I meant intuitive like easy to understand for humans. (It is also intuitionistic but that's a technical fact shared by both Coq and Agda (though not HOL)). The reason I said that is because thinking in terms of types is very straightforward for people. "Give me a View and Serializer so I can give you JSON" "Why is my code not working? Oh because you can't always find the head of a list, I need to give you NonEmpty List T". Similarly, proving something is a group is like trying to go Group somehow from the objects around.
ah, my bad, i see how that makes more sense. FWIW i agree – often, mentally converting a theorem to a type and thinking about the problem in that framework makes things easier for me to grasp. (also explains why we "apply" theorems/lemmas :) )
"Optimality, no garbage-collection, EVM and GPU compatibility are all possible due to compilation to the symmetric interaction calculus, a lightweight computing model that combines good aspects of the Turing Machine and the Lambda Calculus. In order for this to work, Formality enforces some compile-time restrictions based on Elementary Affine Logic."
Do you have any posts explaining how this avoids GC? At first, it seemed to be that the underlying calculus only uses variables once, but in your examples variables are sometimes repeated. How do the two relate?
The creator (@SrPeixinho) answered some questions on the Haskell subreddit [1]. Looks like you can "box" (his term) variables to allow duplication/copying and it's all tracked statically somehow. (or will be - not sure if that part is fully implemented).
Linear logic and affine logic (the latter of which SrPeixinho refers to in that Reddit post) let you use an assumption only once in a proof. Their counterparts in functional programming are called linear and affine types [0]; the arguments of functions with such types are restricted to being used only once in the function’s body. This constraint lets you do some interesting things in compiling and optimizing languages built around these types, and in particular it makes garbage collection trivial.
Linear and affine types are pretty hot right now in the small world of type theory and functional programming. SrPeixinho’s work with his collaborators is aimed at building a language for the Ethereum VM that might actually make it possible to write smart contracts that don’t blow up in your face. It’s good stuff. Search his posts on Reddit to see what he’s up to [1].
I think affine types force usage at least once, while linear types force it exactly once. IIRC, this is because linear logic rejects both contraction and weakening while affine logic rejects only contraction.
I'm not sure exactly how this ties into avoiding a GC, but my guess is that rejecting type contraction allows a kind of "reference counting" at the type level.
I was trying to avoid being too detailed, but the distinction is actually that linear types require function arguments to be used exactly once and affine types require that they be used at most once. So affine types allow constant functions, but linear types don’t. A good place to start for anyone interested in learning more is the Wikipedia article on substructural types [0].
And, yes, you’re right that these type systems effectively implement reference counting at the type level. In practice, linear and affine types are used alongside more general types to permit controlled copying and destruction, which tends to look like manual (but type-enforced) memory allocation and deallocation around the edges.
Yes, having separate "sub-languages" for types and terms is a hindrance if we want to have types which depend on values (AKA dependent types).
Besides the obvious advantage that we only need one language, we can also get away with using a single abstraction form (dependent functions) to implement both normal functions and type variables (e.g. "big lambdas" in SystemF).
There are still reasons we might want to avoid doing everything with dependent functions: in particular, it's not obvious (or possibly even decidable) whether a dependent function's argument can be erased or not (i.e. whether parametricity holds for that argument). For this reason Conor McBride has argued that languages should have a parametric "forall" quantifier (like Haskell's existing type variables) as well as the "pi" quantifier found in dependently typed languages (e.g. https://www.reddit.com/r/haskell/comments/390dyx/conor_mcbri... ).
Note that both quantifiers would still be used within one language, and both could be used with both types and values.
I'm not sure how/whether substructural types/logics like the linear and affine features of this language would interact with this distinction though.
They are, and that is one of the nice things of a type system like this. (I believe that's the "dependent types" bit.) It lets you express quite powerful theorems about (simple?) programs without having to stray too far from the language.
