zlacker

the fact that most of Co-Pilot's usefulness comes from repeating common snippets of code makes me think there has to be a much simpler way to reduce the boilerplate of "common tasks"

>>ausbah+(OP)
In my opinion, dependent type systems are that way.

A dependent type is a type that depends on a value. What something is depends on something else; What something is is derived from something else – with computation. What dependent types are are calculations of type structure.

Unbounded, this becomes intractable like all unbounded computational expressivity. So that’s what modern dependent type systems need to solve—and they do. There exist formal results that frame the computational expressivity of dependent type systems and make perfectly feasible and tractable the task of deriving significantly complex types. Automatically.

The Idris language is a great example of where we’re heading.

The reason I’m more interested in this sort of thing rather than Copilot is that dependent type systems are based on formally rigorous methods. You end up with formally verified programs, by way of the same mechanisms that allow you to derive them automatically. They’re also easier to compose, for the same reasons.

Edwin Brady’s Idris demonstratons on Youtube show a bit of what’s possible. In one, the compiler automatically writes a formally-correct type-directed matrix multiplication function. In another, run-length encoding and decoding functions are generated from a type definition.

The book Type-Driven Development with Idris is a great read. Mind-expanding.

Programming is automation. The automation of automation is… dependent types.

>>ausbah+(OP)
Why? I haven't used it but it seems like the only reason it is good at repeating common snippets of code is because it is so clever. I don't think a simpler solution would be possible because it isn't exactly repeating code (except in contrived examples). It's adapting it to the context.

>>Anthon+c4
Formally rigorous methods have almost always lost out in the market against slop like JavaScript.

I think the reasons are completely pragmatic and boil down to two things.

The first is that rigorous systems usually take longer to build and meanwhile the slop ships first and gains mindshare.

The second is that rigorous systems are usually built by academics or specialists in some specific vertical and lack the easy installation, easy onboarding, and integration with other platforms that more pragmatic sloppy platforms tend to prioritize first. Those things get prioritized first because sloppy languages and systems tend to evolve from makeshift "shop jigs" used to get stuff done, not from research.

>>ausbah+(OP)
common lisp's macros are the most powerful abstraction. that said, its a VERY sharp tool

>>api+7a
I see this too!

I think Edwin Brady also does.

Idris code is short and clear.

There is much less of it – for instance, as a kind overly specific example, serializers/deserializers and API code can be automatically generated from the model definition.

Idris code tends to sort of “fold in” test code into the function definitions themselves, so you do less work AND it’s much more rigorous.

Then there’s the compiler IDE interface which is explicitly intended to be an upstanding citizen in developer workflows.

I also want to mention how easy it is to write Idris compiler backends for any given language. This is on purpose, and is made possible by what Idris is: It’s dependent types, and dependent types is automation of the automation.

So it’s not a question of “making muggle developers eat their formal vegetables” or the like. It’s that when the automation of the automation hits, it makes work so much faster and more efficient and more pleasant that it outcompetes the slop because slop is slop. Idris might be that automation; It might not. We’ll see, right?

I’ve picked this hill to die on. At least one death, of something. Maybe just a feeling or a hope, but something.