I like the direction of this post, having similar interests. However, I think the bubble metaphor is weaker than the rest of the argument, and that there are clearer ways to show why it makes sense to adopt formal methods.
Let’s start with the weakness of the bubble metaphor: you don’t go into the externalities, limitations, collaboration and upkeep needed to uphold and maintain a bubble. The world is becoming increasingly standardised, discrete, manageable; yet also increasingly convoluted, non-linear, surprising etc. Keeping up the standards sometimes works as if by magic (clock time seems just part of the territory nowadays). I’m lurking in a protocol research group that is looking into exactly things like this, and it is an interesting and tractable area, but also very messy!
For me, the argument is simpler: To get an AI to produce an artefact, that artefact needs to be specified. We have different ways to specify an artefact, from natural language, to unit testing, to linters, to e2e acceptance test, type-driven programming with algebraic invariants, to user feedback and testing. I’m surely missing some. These specifications can be seen as constraints in program-space, creating an intersection where variations of the produced artefact lives. The more constraints we have, the better. The “harder” our constraints are (as in not budging, not being flexible), the better. Formal specification is a way to make natural language harder, a better constraint. Nuff said :)
In my mind, the reason we don’t have pervasive property testing, algebraic laws, strongly typed systems, well-designed programming languages etc, is because adoption requires onboarding, which is costly. I hope ai will change the picture.
Thanks for zeroing in on a tricky idea that I could use help articulating and arguing for. I certainly agree that requirements that impose additional constrains make it safer to use automatic code generators, and the broader economic context does not need to change to make that statement true.
I think it is a fascinating question for study whether increasing uptake of AI will reduce the tendency of the world to become “increasingly convoluted, non-linear, surprising” in your words—partly because those qualities make it harder to apply AI effectively. Are you personally betting on convolution and surprise increasing? I don’t mean that humans will be surprised; it’s likely we’ll find a world of increased use of AI mind-bending. But will the AIs find that surprise is high and increasing?
I like the direction of this post, having similar interests. However, I think the bubble metaphor is weaker than the rest of the argument, and that there are clearer ways to show why it makes sense to adopt formal methods.
Let’s start with the weakness of the bubble metaphor: you don’t go into the externalities, limitations, collaboration and upkeep needed to uphold and maintain a bubble. The world is becoming increasingly standardised, discrete, manageable; yet also increasingly convoluted, non-linear, surprising etc. Keeping up the standards sometimes works as if by magic (clock time seems just part of the territory nowadays). I’m lurking in a protocol research group that is looking into exactly things like this, and it is an interesting and tractable area, but also very messy!
For me, the argument is simpler: To get an AI to produce an artefact, that artefact needs to be specified. We have different ways to specify an artefact, from natural language, to unit testing, to linters, to e2e acceptance test, type-driven programming with algebraic invariants, to user feedback and testing. I’m surely missing some. These specifications can be seen as constraints in program-space, creating an intersection where variations of the produced artefact lives. The more constraints we have, the better. The “harder” our constraints are (as in not budging, not being flexible), the better. Formal specification is a way to make natural language harder, a better constraint. Nuff said :)
In my mind, the reason we don’t have pervasive property testing, algebraic laws, strongly typed systems, well-designed programming languages etc, is because adoption requires onboarding, which is costly. I hope ai will change the picture.
Thanks for zeroing in on a tricky idea that I could use help articulating and arguing for. I certainly agree that requirements that impose additional constrains make it safer to use automatic code generators, and the broader economic context does not need to change to make that statement true.
I think it is a fascinating question for study whether increasing uptake of AI will reduce the tendency of the world to become “increasingly convoluted, non-linear, surprising” in your words—partly because those qualities make it harder to apply AI effectively. Are you personally betting on convolution and surprise increasing? I don’t mean that humans will be surprised; it’s likely we’ll find a world of increased use of AI mind-bending. But will the AIs find that surprise is high and increasing?