In the thing I am making, you can't have a variable without choosing a specific example value for that variable. This is surely something that's been discussed here before since Bret does it in Inventing On Principle. What do folks think of it?

I came here to say programming by example, but I see you already mentioned it 🙂 as long as it works for your tool, I find it really nice, you can't build invalid things since you are always referencing a valid example

This is such a complicated and cool question and I have so many thoughts I don’t even know where to begin. I remember watching your talk about the thing you’re making and I think you mentioned something along these lines being one of the big problems. I was surprised you wanted to be able to prove theorems in this system because of course a visual environment and proofs have this tension. I’m curious what kind of proofs you would have in this system. In the video you mentioned a theorem in quantum computing(?) but I couldn’t find it. As an elementary but nontrivial example how would you prove the Pythagorean theorem? I think you would have to do this abstractly, but as long as it is “constructive” you can unfold the abstract proof at various stages and apply it to specific vectors to visualize it. Also, if you are doing proofs I imagine these would be “formal proofs” and isn’t that a really tough problem? Or do I misunderstand or is there some way to get around it? eg just have a more expressive and dynamic means to write informal proofs. Anyway I certainly wouldn’t shy away from general variables as long as you have a means to move up and down the ladder of abstraction 😉.

Starting from concrete values, you can approach abstraction by lifting from a single value to many at once. Remember Bret's Ladder of Abstraction. For extra fun, have interactions between the multiple values. For instance, instead of a solution set of values that would work in a given context, have a probability distribution. I was pretty into these propagation networks at once point https://dspace.mit.edu/handle/1721.1/49525. Don't know if more progress has been made.

In Glamorous Toolkit, examples play a key role. We went so far as to replace classic tests with examples (a test that returns an object). This leads to a nicer way to compose examples, but most importantly, examples offer concrete objects you can program against. As in our environment every object can present itself through custom views and as these views can also be weaved into larger narratives, the examples also offer a nice infrastructure for documentation purposes. Here is a short article about them: https://medium.com/feenk/an-example-of-example-driven-development-4dea0d995920

@Robin When you say that it is "obvious" that visual environments and proofs have a tension, I guess (?) you mean that visual proofs are criticized as being not as rigorous as algebraic, because it seems to be more about intuition. This is an interesting philosophical issue and may end up being a problem for me, but I'm willing to bet that it will be sufficiently non-small The kinds of proofs I am interested to give are (as you'd expect) fundamentally GA-related, so for example, proving that rxr* is a rotation when r is a rotor and r* is its reverse and x is a vector. Or, expanding a bit, classical mechanics, so proving that ellipses are solutions to the two-body problem. And yes, if I get to it, quantum computing! Subalgebra closure is probably what you were thinking of. It wouldn't be super surprising if the system ends up somewhere in between "strong enough to prove pythagorean theorem" and "strong enough to prove QM subalgebra closure" "How would you prove the pythagorean theorem?" Thanks a lot for asking me that question, it's a great example to start with and I'd not thought about it :D and now I've thought about it and I know how to prove it. It's a combination of defining a "right angled triangle" by the constraints that are on it (which are visual) and then applying the rules of geometric algebra, which are all visual, to that constraint. I can say more but it might just sound weird/spoil the fun when you eventually see it 😛

@hamish todd By the tension I meant, just the problem you brought up in the original post in this thread, and as I was watching your video that was the question that crossed my mind. Can’t wait to see what you cook up!

incidentally, some kind of geometric algebra conference popped up on my subscribed youtube feed this morning: https://www.youtube.com/user/EnkiOrigami

Yes, it is hoped that that conference will have a significant impact!

let me know when the “GA for absolute morons” lecture comes out and i will become an enthusiastic proponent!

It will be a while, I want to make it really good 😅