The future of interactive theorem proving?

The future of interactive theorem proving?
xenaproject.wordpress.com

I would love for computers to be able to understand informal but rigorous mathematical reasoning, but, having worked with current proof assistants, it sure feels like software design will have to be solved in the same sense first.

That said, kudos for an awesome demo!

SQL is the great success story of that generation.

Writing database query and management code in an imperative language is a nightmare.

While it's an undeniable achievement that these kinds of models can generate syntactically correct code or even the correct solution some of the time. I find it hard to get excited about them for anything but boilerplate (and even they I think they pose the greatest risk, lulling one into a false sense of security until you get bitten).

If we take formal methods as the way to ensure the code we've written provably does what we say it does, we had better damn well make sure that what we've said it does is what we want it to do. In other words, I feel like this is offloading the most important part of the problem, and the one that can't be checked automatically onto a very iffy situation.

We should really stop to consider what these kinds of models are. Pattern recognizers, not thinking machines. See the author's quote about this theorem:

    Let G be a Lie group. Then the tangent space at the identity is a Lie algebra.

    theorem tangent_space_at_identity_is_lie_algebra (G : Type*) [group G]
      [topological_space G] [topological_group G] [charted_space G] [smooth_manifold G] :
        lie_algebra (tangent_space_at_identity G) :=

    For some completely unclear reason, the app decides to consider a Lie algebra over \mathbb{R} instead of my explicit instruction to use a field k, and that’s even before addressing the fact that tangent_space_at_identity is not a mathlib definition. I tried a few different responses to the app’s initial attempt, and couldn’t get it to do anything helpful.

    You must specify a field for your Lie algebra as in lie_algebra k M

    lie_algebra R (tangent_space_at_identity G) :=

I guess my point hinges completely on what you consider "knowing" to be. It's kind of funny. Nobody would ever say that a compiler knows how to transform one language to another. The personification of ML really irks me. I try very hard to avoid it, but it's easy to slip.

I don't want to say we should throw the baby out with the bathwater. I do think that there are uses for these things. The recognition of the pattern for the syntax to specify the characteristics of a Lie group would make a great first pass at a snippet template. (This is ignoring the question of why isn't Lie_group a definition that just pulls in the necessary requirements on G rather than needing to specify them each time. If one of those is not really a requirement for Lie groups, forgive me, my exposure to Lie theory is very limited.)

I would be much more interested in a tool that allows me to identify patterns in the code with a summary printout or something like the likelihood of a given pattern in the neighborhood of my cursor. The generation part is just not good enough to trust IMO.

Also, I really hope we see some sort of backlash for MS just deciding to just ignore everyone's' licenses.