7 ms·

RDL: a lightweight system for adding contracts to Ruby

81 points by muhic 10y ago

chrisseaton 10y ago
RDL supports most of the serious research anyone is doing into types in Ruby. See the papers with Foster as an author under Types here http://rubybib.org http://rubybib.org. I hope the Ruby core team is watching their progress since some kind of typing is being debated by Matz.
- ksec 10y ago
  That is "the" problem, "how" do we know if the Core Team are watching / discussing / debating. Comparing a similar situation to the Python circle ( You can laugh about Python 3 all you want, but that is another issue ), which is clearly layout and in some way beautifully presented.
dkarapetyan 10y ago
This is fantastic. They even have type checking. Looking forward to the day this turns into something like tsc.
smizell 10y ago
Very cool. I experimented with something similar in JavaScript. https://github.com/smizell/snug https://github.com/smizell/snug For me, it is useful for runtime checking data that may come across the web.
metafex 10y ago
Oh wow, even with support for static type-checking. It really makes me want to give ruby another shot. Piggybacking on this: apart from F*, does someone know of a language or support for existing ones for contracts, loop-invariants and possibly verification? Dafny and Spec# aren't very general-purpose and apart from those nothing much comes to my mind.
- losvedir 10y ago
  When I think of contracts, I think of Eiffel. Not really sure how much it's actually used, though. Also, maybe Ada? I always wonder why Ada doesn't get any love on HN.
  - pjmlp 10y ago
    Given that the company is still around, I would say that they manage to have a set of customers that value the language and what it offers in terms of quality.
- david-given 10y ago
  Ada has robust preconditions and postconditions. Untested code follows: procedure swap(a: in out integer, b: in out integer) with pre => a <> b -- just for example purposes post => (a == b'old) and (b == a'old) is declare t: integer; begin t := a; a := b; b := t; end (Sorry, couldn't think of a sensible small example which uses both pre and post, hence the terrible precondition.) Note that the postcondition can refer to the old values of the variables with the 'old suffix --- the values will be automatically saved on entry to the function and used for comparison later. Unfortunately the pre- and postconditions have to be specified in the public part of the module, so can't see any private module variables, which forces you to jump through hoops if you don't want to expose your module's internal state (e.g. checking to make sure that functions on a state machine are called in the right order). You also get type invariants, where you can specify an expression which must always be true for a number: subtype Even is integer with dynamic_predicate => (Even mod 2) == 0; Or, if you really want your mind blown: subtype Even is integer with dynamic_predicate => (for some N in integer => (Even == N*2)); There's also a static_predicate form which only supports a restricted predicate expression but which can be checked at compile time.
  - metafex 10y ago
    Thank you for the example. Also: SPARK is another one I forgot. I guess I'll have to think of a nice example and just implement it in a Ada, F* and with RDL to get a hang of the differences and features.
phpnode 10y ago
It's always baffled me why more people don't seem interested in adopting design by contract, it is a ridiculously powerful tool for writing quality software. Here's a Babel plugin which adds design by contract to JavaScript, squeezing it into existing JS syntax (the result is really similar to Eiffel) - https://github.com/codemix/babel-plugin-contracts https://github.com/codemix/babel-plugin-contracts and here's what it looks like in a reasonably complicated program - https://github.com/codemix/malloc/blob/master/src/index.js https://github.com/codemix/malloc/blob/master/src/index.js (disclosure: I wrote this)
- jonahx 10y ago
  This looks cool. Where do you see this fitting in versus using something like TypeScript or PureScript?
  - phpnode 10y ago
    It's definitely most useful when combined with type annotations. They're complementary tools, annotations can ensure type safety at compile time, but type safety is only one part of program correctness, whereas contracts can validate just about any aspect of program operation because they have access to all of the runtime information. They're like unit tests that run all the time (until you strip them in production at least). This thing can be used alongside Flow[0] and other babel plugins which use flow syntax. [0] https://flowtype.org/ https://flowtype.org/
- spriggan3 10y ago
  > It's always baffled me why more people don't seem interested in adopting design by contract Because it's yet another layer on top of other layers, because it has performance implications ... A few languages such as Vala support some form of contracts, this kind of feature is more useful when part of the language itself, not some third party babel plugin that leads to codebase fragmentation as one just had yet another layer to the compilation pipeline. No offense, that's a nice thing you wrote, I'm just not going to use this kind of thing and add more complexity for very little gain. To me tests ARE the contracts. I would only be willing to pay the cost of transpilation with something like Typescript which adds a signification value. Babel and co ? not worthwhile.
echelon 10y ago
Typing is such an important and powerful construct. It'd be amazing if scripting languages like Ruby and Python built optional typing into future versions, especially if they could be used in speeding up the execution time. If nothing else, type safety for function signatures would be a huge win for productivity, testing, and would cut down on a large class of programmer-introduced bugs.
- unsignedqword 10y ago
  https://docs.python.org/3/library/typing.html https://docs.python.org/3/library/typing.html https://bugs.ruby-lang.org/issues/9999 https://bugs.ruby-lang.org/issues/9999
- pmontra 10y ago
  I used languages with static types for half of my professional life, the last one was Java, and languages with dynamic types in the other half. I never felt like I have more bugs in dynamic typed languages. What I felt is that I don't have to waste time writing stuff like ArrayList<Whatever> when just something = {} works perfectly well in practice. I understand that many people say that with static typing if it compiles it works, but I remember using debuggers quite a lot. I'd say that if one wants types there are plenty of languages to choose from. There is Crystal if one likes Ruby. Contracts are interesting. I remember Eiffel and other languages. Those could be useful regardless of the kind of typing the language use. BTW, invariants are another useful tool when designing some algorithms and were neglected recently.
  - bjz_ 10y ago
    > I never felt like I have more bugs in dynamic typed languages. What I felt is that I don't have to waste time writing stuff like ArrayList<Whatever> when just something = {} works perfectly well in practice. Java is a pretty terrible language when it comes to static types. If you have a language that allows you to work with types in a succinct and expressive way, you end up with a powerful modelling tool that can help you reason about and design programs. The side-effect of this is to have far less runtime crashes (you know what cases to check for, like nullable data), great documentation for your future self and your fellow devs, and a greater liberty to do large scale refactors without worrying about breaking things.
programminggeek 10y ago
Don't get too excited. It's not rails enough for the ruby community to ever seriously use it. I know this from firsthand experience going down the same rabbit hole a few years ago.
- thomasluce 10y ago
  Yeah. I made a ruby gem a while back that did this, but with rdoc strings instead ( I hated docs getting out if line with functionality) called "contraction". The code isn't the greatest, and I would probably do things a bit different now, but it worked. More railsy , for sure, but I don't know if that actually made it better...
- ksec 10y ago
  >rails enough Cant upvote you enough. I am getting the sense that DHH dictates more of Ruby rather then Matz. ( Which isn't necessarily a good or bad thing )
woodruffw 10y ago
Good to see PLUM (Programming Languages at the University of Maryland) releasing their work on GitHub. They're among the most talented in the department at UMD.
- socrates1024 10y ago
  Totally. PLUM is a great team, and this work on ruby contracts from Brianna and Jeff is particularly awesome. By the way, their newest paper about the work in this github is going to be at PLDI: https://www.cs.umd.edu/~jfoster/papers/pldi16.pdf https://www.cs.umd.edu/~jfoster/papers/pldi16.pdf (disclaimer: I just graduated from PLUM)
  - woodruffw 10y ago
    Awesome, thanks for sharing! And congratulations on graduating. I'm an undergraduate, so my experience with PLUM is just that of an admirer looking in ;)
bjz_ 10y ago
Anyone know what the performance implications for using this would be?
Dangeranger 10y ago
After changing focus from Ruby to functional languages recently I've found that optional types can be really helpful in a lot of situations. Ruby also has another popular and mature library that I am surprised nobody has mentioned yet named 'Contracts.ruby' https://github.com/egonSchiele/contracts.ruby https://github.com/egonSchiele/contracts.ruby This syntax is also more appealing to my eyes than what rdl provides. Contract Num => Num def double(x) x * 2 end
nurettin 10y ago
I wonder if contracts can be used to speed up the execution instead of slowing it down.
arunix 10y ago
Some differences from Eiffel contracts: no class invariants, and postconditions don't have access to previous object state.

81 points by muhic 10y ago

RDL supports most of the serious research anyone is doing into types in Ruby. See the papers with Foster as an author under Types here http://rubybib.org http://rubybib.org. I hope the Ruby core team is watching their progress since some kind of typing is being debated by Matz.

ksec 10y ago
That is "the" problem, "how" do we know if the Core Team are watching / discussing / debating. Comparing a similar situation to the Python circle ( You can laugh about Python 3 all you want, but that is another issue ), which is clearly layout and in some way beautifully presented.

dkarapetyan 10y ago

This is fantastic. They even have type checking. Looking forward to the day this turns into something like tsc.

smizell 10y ago

Very cool. I experimented with something similar in JavaScript. https://github.com/smizell/snug https://github.com/smizell/snug For me, it is useful for runtime checking data that may come across the web.

metafex 10y ago

Oh wow, even with support for static type-checking. It really makes me want to give ruby another shot. Piggybacking on this: apart from F*, does someone know of a language or support for existing ones for contracts, loop-invariants and possibly verification? Dafny and Spec# aren't very general-purpose and apart from those nothing much comes to my mind.

losvedir 10y ago
When I think of contracts, I think of Eiffel. Not really sure how much it's actually used, though. Also, maybe Ada? I always wonder why Ada doesn't get any love on HN.
- pjmlp 10y ago
  Given that the company is still around, I would say that they manage to have a set of customers that value the language and what it offers in terms of quality.
david-given 10y ago
Ada has robust preconditions and postconditions. Untested code follows: procedure swap(a: in out integer, b: in out integer) with pre => a <> b -- just for example purposes post => (a == b'old) and (b == a'old) is declare t: integer; begin t := a; a := b; b := t; end (Sorry, couldn't think of a sensible small example which uses both pre and post, hence the terrible precondition.) Note that the postcondition can refer to the old values of the variables with the 'old suffix --- the values will be automatically saved on entry to the function and used for comparison later. Unfortunately the pre- and postconditions have to be specified in the public part of the module, so can't see any private module variables, which forces you to jump through hoops if you don't want to expose your module's internal state (e.g. checking to make sure that functions on a state machine are called in the right order). You also get type invariants, where you can specify an expression which must always be true for a number: subtype Even is integer with dynamic_predicate => (Even mod 2) == 0; Or, if you really want your mind blown: subtype Even is integer with dynamic_predicate => (for some N in integer => (Even == N*2)); There's also a static_predicate form which only supports a restricted predicate expression but which can be checked at compile time.
- metafex 10y ago
  Thank you for the example. Also: SPARK is another one I forgot. I guess I'll have to think of a nice example and just implement it in a Ada, F* and with RDL to get a hang of the differences and features.

phpnode 10y ago

It's always baffled me why more people don't seem interested in adopting design by contract, it is a ridiculously powerful tool for writing quality software. Here's a Babel plugin which adds design by contract to JavaScript, squeezing it into existing JS syntax (the result is really similar to Eiffel) - https://github.com/codemix/babel-plugin-contracts https://github.com/codemix/babel-plugin-contracts and here's what it looks like in a reasonably complicated program - https://github.com/codemix/malloc/blob/master/src/index.js https://github.com/codemix/malloc/blob/master/src/index.js (disclosure: I wrote this)

jonahx 10y ago
This looks cool. Where do you see this fitting in versus using something like TypeScript or PureScript?
- phpnode 10y ago
  It's definitely most useful when combined with type annotations. They're complementary tools, annotations can ensure type safety at compile time, but type safety is only one part of program correctness, whereas contracts can validate just about any aspect of program operation because they have access to all of the runtime information. They're like unit tests that run all the time (until you strip them in production at least). This thing can be used alongside Flow[0] and other babel plugins which use flow syntax. [0] https://flowtype.org/ https://flowtype.org/
spriggan3 10y ago
> It's always baffled me why more people don't seem interested in adopting design by contract Because it's yet another layer on top of other layers, because it has performance implications ... A few languages such as Vala support some form of contracts, this kind of feature is more useful when part of the language itself, not some third party babel plugin that leads to codebase fragmentation as one just had yet another layer to the compilation pipeline. No offense, that's a nice thing you wrote, I'm just not going to use this kind of thing and add more complexity for very little gain. To me tests ARE the contracts. I would only be willing to pay the cost of transpilation with something like Typescript which adds a signification value. Babel and co ? not worthwhile.

echelon 10y ago

Typing is such an important and powerful construct. It'd be amazing if scripting languages like Ruby and Python built optional typing into future versions, especially if they could be used in speeding up the execution time. If nothing else, type safety for function signatures would be a huge win for productivity, testing, and would cut down on a large class of programmer-introduced bugs.

unsignedqword 10y ago
https://docs.python.org/3/library/typing.html https://docs.python.org/3/library/typing.html https://bugs.ruby-lang.org/issues/9999 https://bugs.ruby-lang.org/issues/9999
pmontra 10y ago
I used languages with static types for half of my professional life, the last one was Java, and languages with dynamic types in the other half. I never felt like I have more bugs in dynamic typed languages. What I felt is that I don't have to waste time writing stuff like ArrayList<Whatever> when just something = {} works perfectly well in practice. I understand that many people say that with static typing if it compiles it works, but I remember using debuggers quite a lot. I'd say that if one wants types there are plenty of languages to choose from. There is Crystal if one likes Ruby. Contracts are interesting. I remember Eiffel and other languages. Those could be useful regardless of the kind of typing the language use. BTW, invariants are another useful tool when designing some algorithms and were neglected recently.
- bjz_ 10y ago
  > I never felt like I have more bugs in dynamic typed languages. What I felt is that I don't have to waste time writing stuff like ArrayList<Whatever> when just something = {} works perfectly well in practice. Java is a pretty terrible language when it comes to static types. If you have a language that allows you to work with types in a succinct and expressive way, you end up with a powerful modelling tool that can help you reason about and design programs. The side-effect of this is to have far less runtime crashes (you know what cases to check for, like nullable data), great documentation for your future self and your fellow devs, and a greater liberty to do large scale refactors without worrying about breaking things.

programminggeek 10y ago

Don't get too excited. It's not rails enough for the ruby community to ever seriously use it. I know this from firsthand experience going down the same rabbit hole a few years ago.

thomasluce 10y ago
Yeah. I made a ruby gem a while back that did this, but with rdoc strings instead ( I hated docs getting out if line with functionality) called "contraction". The code isn't the greatest, and I would probably do things a bit different now, but it worked. More railsy , for sure, but I don't know if that actually made it better...
ksec 10y ago
>rails enough Cant upvote you enough. I am getting the sense that DHH dictates more of Ruby rather then Matz. ( Which isn't necessarily a good or bad thing )

woodruffw 10y ago

Good to see PLUM (Programming Languages at the University of Maryland) releasing their work on GitHub. They're among the most talented in the department at UMD.

socrates1024 10y ago
Totally. PLUM is a great team, and this work on ruby contracts from Brianna and Jeff is particularly awesome. By the way, their newest paper about the work in this github is going to be at PLDI: https://www.cs.umd.edu/~jfoster/papers/pldi16.pdf https://www.cs.umd.edu/~jfoster/papers/pldi16.pdf (disclaimer: I just graduated from PLUM)
- woodruffw 10y ago
  Awesome, thanks for sharing! And congratulations on graduating. I'm an undergraduate, so my experience with PLUM is just that of an admirer looking in ;)

bjz_ 10y ago

Anyone know what the performance implications for using this would be?

Dangeranger 10y ago

After changing focus from Ruby to functional languages recently I've found that optional types can be really helpful in a lot of situations. Ruby also has another popular and mature library that I am surprised nobody has mentioned yet named 'Contracts.ruby' https://github.com/egonSchiele/contracts.ruby https://github.com/egonSchiele/contracts.ruby This syntax is also more appealing to my eyes than what rdl provides. Contract Num => Num def double(x) x * 2 end

nurettin 10y ago

I wonder if contracts can be used to speed up the execution instead of slowing it down.

arunix 10y ago

Some differences from Eiffel contracts: no class invariants, and postconditions don't have access to previous object state.