8 ms·

I find the introduction interesting, it somehow clicked. Devs are like toddlers playing with wooden bricks, who are demanded to scale up this act of building t

I find the introduction interesting, it somehow clicked. Devs are like toddlers playing with wooden bricks, who are demanded to scale up this act of building to the level of a grown up's house. In fact it often feels that way. You're either asked to extend or improve existing constructions that feel like sticks and stones bound together with rubber bands. Or one feels excited for being allowed to make up such a construction as a demo, not knowing it will be used as a basis for a production-quality construction. I'm not sure if mathematical proof is the way to go. There's just too much code to cover for this approach to be realistic. Most problems are born on the drawing table. The designs seem right on paper and only in practice, during or after building, they become visable.

zmgsabst 3y ago
Turning a foam architectural model into a house without the required cost investment because the foam model was “so quick to make” feels like a frustratingly accurate description.
brigadier132 3y ago
Yep, we build a foundation with plywood and styrofoam and then someone comes and asks you to build a skyscraper on top of it.
- trwaw 3y ago
  We build a train and then someone asks to turn it into a skyscraper because skyscrapers are the in thing now. It already looks like one on its side, how hard can it be to turn it right side up?
- smaudet 3y ago
  While I do think proof constructed code could be superior, I am not convinced for two reasons: 1. The problem expressed here has to do with a particular, well understood problem. It is not subject to the whims or constraint needs of the "customer". Proof construction is great when the problem is properly understood, I don't know how well it handles constantly changing requirements. (This encompasses business and interaction constraints too - perhaps you can construct a provable correct UI, but will it be engaging or usable?) 2. Test driven development can guide high quality code construction, arguably at lower construction cost. That is the reason I'd argue this has not taken off in comparison to traditional "test" based design. You can argue it produces lower quality code, and you'd probably be right. But in comparison to construction of complex, rich design, I suspect that it produces faster results at lower cost. The provable solution will win out...eventually. Depends on whether it can make significant marker penetration once it is complete. Nevertheless, yes of course we should be building foundations witb concrete not plywood and Styrofoam, so this is a good development. I do think a proper engineering approach with test based verification can build a "somewhat concrete" foundation, at least.
deleted 3y ago
[deleted]
mrkeen 3y ago
> I'm not sure if mathematical proof is the way to go. There's just too much code to cover for this approach to be realistic. It may be unrealistic, but people are doing it anyway. It may be the case that there are just a few Leslie Lamports capable of doing this stuff, and it's unrealistic to expect the rest of us to. But even if that's the case, I still want them to publish their code as libraries, so I can reach for tools that will work - even if I couldn't have proved it myself. And if this whole mathematical/proofy way of doing things is a dead end (which I strongly disagree with - we're just at the beginning!) then it's no big deal, because we are already really good at turning JSON into stack traces.

zmgsabst 3y ago

Turning a foam architectural model into a house without the required cost investment because the foam model was “so quick to make” feels like a frustratingly accurate description.

brigadier132 3y ago

Yep, we build a foundation with plywood and styrofoam and then someone comes and asks you to build a skyscraper on top of it.

trwaw 3y ago
We build a train and then someone asks to turn it into a skyscraper because skyscrapers are the in thing now. It already looks like one on its side, how hard can it be to turn it right side up?
smaudet 3y ago
While I do think proof constructed code could be superior, I am not convinced for two reasons: 1. The problem expressed here has to do with a particular, well understood problem. It is not subject to the whims or constraint needs of the "customer". Proof construction is great when the problem is properly understood, I don't know how well it handles constantly changing requirements. (This encompasses business and interaction constraints too - perhaps you can construct a provable correct UI, but will it be engaging or usable?) 2. Test driven development can guide high quality code construction, arguably at lower construction cost. That is the reason I'd argue this has not taken off in comparison to traditional "test" based design. You can argue it produces lower quality code, and you'd probably be right. But in comparison to construction of complex, rich design, I suspect that it produces faster results at lower cost. The provable solution will win out...eventually. Depends on whether it can make significant marker penetration once it is complete. Nevertheless, yes of course we should be building foundations witb concrete not plywood and Styrofoam, so this is a good development. I do think a proper engineering approach with test based verification can build a "somewhat concrete" foundation, at least.

deleted 3y ago

[deleted]

mrkeen 3y ago

> I'm not sure if mathematical proof is the way to go. There's just too much code to cover for this approach to be realistic. It may be unrealistic, but people are doing it anyway. It may be the case that there are just a few Leslie Lamports capable of doing this stuff, and it's unrealistic to expect the rest of us to. But even if that's the case, I still want them to publish their code as libraries, so I can reach for tools that will work - even if I couldn't have proved it myself. And if this whole mathematical/proofy way of doing things is a dead end (which I strongly disagree with - we're just at the beginning!) then it's no big deal, because we are already really good at turning JSON into stack traces.