I mean, create a new language, but you don't really need to push the dependent type agenda up front - just say you have an 'expressive type system'. You already have motivating examples because they're in the libraries and example applications. Can expand on the theory later.
-
-
I think if you have them, the machinery is going to be pretty visible and you might as well own it / advertise it. They’re immensely powerful! Like time-lord, Jean Grey, space-folding over-9000 powerful. Just … not without costs, maybe overkill for that todo-list app.
1 reply 0 retweets 3 likes -
It depends on the approach, I suspect. Even Jean Grey wasn't always Phoenix, to use your metaphor. Looking at ways to bend the curve towards usability may be a way to incorporate dependent types without requiring a large upfront time investment by the library consumers.
1 reply 0 retweets 2 likes -
It’s not the usability that concerns me; that’s interesting and ongoing work. I’m concerned that the entire task they’re useful for (of stating, much less proving fine-gained invariants) isn’t sufficiently appealing/motivated for mainstream programming problems.
3 replies 0 retweets 2 likes -
Replying to @graydon_pub @jntrnr and
I mean maybe if there’s a sea change in the legal environment and we can no longer get away with shipping code as we do? It’s always conceivable. But it’d be a different world. Most programs written today have only very weak associated meanings of correctness.
1 reply 0 retweets 2 likes -
This is a different topic. While it maybe useful to try to imagine that future, your thesis that DT is very powerful is a good kicking off point. From there, showing what that power can do, with a framework that's usable, you wouldn't need a sea change to attract users.
1 reply 0 retweets 0 likes -
My point is that the "what's possible" part covers principally activities that most users don't want to do: express and prove complex system invariants. It's not at all clear what those are for most programs, and the effort to define them gets you nowhere closer to "shipping".
1 reply 0 retweets 3 likes -
Replying to @graydon_pub @jntrnr and
It would, IOW, take a major shift to the economic priorities of people working in software. Maybe that might happen (I'd love it if it did) but I'm not seeing much sign of it yet.
1 reply 0 retweets 2 likes -
Jonathan Turner Retweeted Patrick Walton
Sounds like
@pcwalton is thinking along similar lines (https://twitter.com/pcwalton/status/1029587679732588544 …) All said, this doesn't seem to help@pigworker with his original question. Instead, it seems to redouble the "worthless" feeling he mentions. Are there creative solutions here to show the value?Jonathan Turner added,
2 replies 0 retweets 0 likes -
Replying to @jntrnr @graydon_pub and
Well, to the original question, I’d answer: Focus on the niche of widely-used, core infrastructure code where the cost of a bug is really high. Ignore Web apps and so forth (for now, anyway). Prove your filesystem driver correct, or your malloc implementation, etc.
2 replies 0 retweets 5 likes
Prove a JIT and a garbage collector correct (and make them acceptably fast) and you’ll have browser vendors beating down your door :)
-
-
I've had a ( impossible?) dream for a while of a DTish subset of rust which isn't exposed in inter-crate APIs which allows the edges of a crate to validate inputs at runtime against a contract which allows safe indexing, dispatch, etc without runtime checks deeper in the crate
1 reply 0 retweets 0 likes -
something something typestate? idk how related that was, I came around long after it. I don't have a clue to what extent this idea is possible, but I've had several occasions where I would have reached for it if it existed
1 reply 0 retweets 0 likes - 1 more reply
New conversation -
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.