Possibly hot take: the “case splitting” approach to program development via interactive program synthesis from extremely specific types has all the same problems that modifying and checking in generated code does, and we all learned why that was a bad idea a long time ago.
-
-
Replying to @lexi_lambda
Are you criticising the Agda/Idris style 'auto-hole-driven development' because using it to modify code may require deleting large portions of code and going through the motions to re-synthesise it for the new specification?
2 replies 0 retweets 3 likes -
Replying to @ielliott95
Alexis King Retweeted Alexis King
Essentially, yes. See https://twitter.com/lexi_lambda/status/1164756359012683778 … and https://twitter.com/lexi_lambda/status/1164869103120728066 …. I don’t think it’s necessarily a bad approach for theorem proving, but I don’t think it is at all sufficient for software development.
Alexis King added,
Alexis King @lexi_lambdaReplying to @mimblewabe @boarders__You’re right, I wasn’t specific enough. I don’t mean the issue is case splitting per se, what I meant was that “with case splitting, the code writes itself” isn’t a sufficient answer to the complaint that you have to write reams of boilerplate when using dependent types.2 replies 0 retweets 5 likes -
Replying to @lexi_lambda @ielliott95
I think the Agda/Idris answer probably involves Haskell-like metaprogramming, and not the Template Haskell kind. You need it already without changing reqs (try writing decidable equality for a large type). And there's some initial work on that! But lots more is needed.
2 replies 0 retweets 0 likes -
The interactive case splitting/program search tooling is only the beginning. We need good refactoring tools, perhaps some way of discovering abstractions, etc. We're on the case but it's not going to be here particularly soon.
1 reply 1 retweet 12 likes -
Replying to @edwinbrady @Blaisorblade and
Was about to say something similar. What people are witnessing is the 'live' development of how-to-program with dependent types. Some current ideas will turn out to be awful. Hopefully they'll be ditched [unlike other PL styles, that never ditch anything].
1 reply 1 retweet 7 likes
I'm very much looking forward to being able to show off live refactoring rather than live programming, and indeed using some live metaprogramming to help. Not that I know how to do that yet. But the criticism is a fair one, as things stand. We have lots to learn.
-
-
Replying to @edwinbrady @jjcarett2 and
Indeed, I should be clear that do not believe the existing tech is at all a dead-end, and in fact I believe it already provides value! I just happened to see the “the boilerplate isn’t actually a big deal because it’s basically auto-generated” argument once too many times.
0 replies 0 retweets 9 likesThanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.