7 ms·

Runtime verification in Erlang by using contracts

138 points by lainon 8y ago

rednerrus 8y ago
"Accidentally" erased footage of the moon landing?!?
- deleted 8y ago
  [deleted]
- thieving_magpie 8y ago
  Wrong thread: https://news.ycombinator.com/item?id=19095849 https://news.ycombinator.com/item?id=19095849
kevintb 8y ago
https://github.com/tamarit/edbc https://github.com/tamarit/edbc for those who want to see the implementation
- reallydude 8y ago
  When trying to write a demonstration of how something works, why not make it expressive, explicit, and dead simple when attempting to demonstrate the utility of something? It just looks like a thunk of code, with little rhyme or reason.
  - BenMorganIO 8y ago
    I gotta agree. The readme itself describes nothing. The code to me feels useless without documentation on how to use it. Otherwise, I have to painstakingly go through their source or read 19 pages of small font. I don't want to do that.
sbabusingh 8y ago
Every time is correct but machine work vreification is no more like human finger work
mhd 8y ago
Some day, after every language has taken its bits, we might actually see Eiffel in the real world. Meanwhile, any of this available for Elixir, too? One of the languages on my 2019 list…
- mrdoops 8y ago
  It's really easy to use Erlang libraries in Elixir. It's nice to be able to tap into an ecosystem with Erlang's maturity while still using modern tooling like Elixir.
- LawnboyMax 8y ago
  I wish Eiffel Software changed their dual licensing business model so that more people would consider using the language in production.
  - hinkley 8y ago
    Bertrand Meyer is constantly at the top of my “people to read when I’ve read all of my unread books” list and unfortunately the last time I looked those books were out of print. My feel at the time was that Meyer introduced Eiffel right on the cusp of the move to free compilers, and he never recovered from that tectonic shift. Whether most developers of that generation could be convinced that rigor was useful I cannot say (but fear the answer is “no”), but they certainly weren’t going to pay to learn or use a new language.
    - pjmlp 8y ago
      We certainly paid for our compilers and interpreters, even to learn a new programming language. Alternative was making our own ones, from code listings. That rigour is useful, having learned Eiffel, coming from Wirth languages background, reading Code Complete, completely influenced my way of writing C and I regularly used all the nice VSC++ ASSERT macros variants for pointer and argument validation. Also adopted code contracts in Java and .NET years later. Coming back to Eiffel, languages need a killer use case for business to adopt them, so they end up only having customers on domains where companies are required to take quality seriously, like high integrity computing.
taude 8y ago
I worked on a large C++ project with design-by-contract pattern a long time ago. It was not the most pleasant experience. There was so much more code to validate pre and post conditions and class invariants. It might have had a lot to do because it was a classic OO business system (think a large Java app now, but where all the code was C++), but I remember spending more time writing the contract code than the actual business code. Is there any recent writings on this pattern on applying the idea more sanely? As it is, I think I prefer to write testing code outside of the core behavior and have to anticipate what values are valid, or create new tests as bugs are found.
- apaprocki 8y ago
  Contracts were developed into the C++ standard to make this easier: https://en.cppreference.com/w/cpp/language/attributes/contract https://en.cppreference.com/w/cpp/language/attributes/contra...
- fiddlerwoaroof 8y ago
  I think in languages like Eiffel that have first-class support for DBC, there’s less noise because the language is designed to propagate contracts appropriately (e.g. making subclasses inherit contracts from their base classes.) Also, there’s been a lot of work in the Racket community on contracts: I think it has something to do with making Racket/Typed Racket interop safe .
- throwawayjava 8y ago
  There's a whole "paradigm" called "light weight verification". I could point to particular papers, but unfortunately I don't know of a good survey article or exemplar tool/implementation/framework. But the term is very google-able, and skimming papers/tool descriptions will quickly give you a general sense for what sort of things are possible.
- macintux 8y ago
  It definitely seems like any OOPL would be inherently at a severe disadvantage in this style. In most Erlang code all you’d have to check are the function parameters. One concern I have with their Erlang solution is that the preconditions and postconditions are expressed for the function as a whole, not each function clause. In some contexts, rather like OOP, a function can be quite different depending on the context it’s called with.

138 points by lainon 8y ago

rednerrus 8y ago

"Accidentally" erased footage of the moon landing?!?

deleted 8y ago
[deleted]
thieving_magpie 8y ago
Wrong thread: https://news.ycombinator.com/item?id=19095849 https://news.ycombinator.com/item?id=19095849

kevintb 8y ago

https://github.com/tamarit/edbc https://github.com/tamarit/edbc for those who want to see the implementation

reallydude 8y ago
When trying to write a demonstration of how something works, why not make it expressive, explicit, and dead simple when attempting to demonstrate the utility of something? It just looks like a thunk of code, with little rhyme or reason.
- BenMorganIO 8y ago
  I gotta agree. The readme itself describes nothing. The code to me feels useless without documentation on how to use it. Otherwise, I have to painstakingly go through their source or read 19 pages of small font. I don't want to do that.

sbabusingh 8y ago

Every time is correct but machine work vreification is no more like human finger work

mhd 8y ago

Some day, after every language has taken its bits, we might actually see Eiffel in the real world. Meanwhile, any of this available for Elixir, too? One of the languages on my 2019 list…

mrdoops 8y ago
It's really easy to use Erlang libraries in Elixir. It's nice to be able to tap into an ecosystem with Erlang's maturity while still using modern tooling like Elixir.
LawnboyMax 8y ago
I wish Eiffel Software changed their dual licensing business model so that more people would consider using the language in production.
- hinkley 8y ago
  Bertrand Meyer is constantly at the top of my “people to read when I’ve read all of my unread books” list and unfortunately the last time I looked those books were out of print. My feel at the time was that Meyer introduced Eiffel right on the cusp of the move to free compilers, and he never recovered from that tectonic shift. Whether most developers of that generation could be convinced that rigor was useful I cannot say (but fear the answer is “no”), but they certainly weren’t going to pay to learn or use a new language.
  - pjmlp 8y ago
    We certainly paid for our compilers and interpreters, even to learn a new programming language. Alternative was making our own ones, from code listings. That rigour is useful, having learned Eiffel, coming from Wirth languages background, reading Code Complete, completely influenced my way of writing C and I regularly used all the nice VSC++ ASSERT macros variants for pointer and argument validation. Also adopted code contracts in Java and .NET years later. Coming back to Eiffel, languages need a killer use case for business to adopt them, so they end up only having customers on domains where companies are required to take quality seriously, like high integrity computing.

taude 8y ago

I worked on a large C++ project with design-by-contract pattern a long time ago. It was not the most pleasant experience. There was so much more code to validate pre and post conditions and class invariants. It might have had a lot to do because it was a classic OO business system (think a large Java app now, but where all the code was C++), but I remember spending more time writing the contract code than the actual business code. Is there any recent writings on this pattern on applying the idea more sanely? As it is, I think I prefer to write testing code outside of the core behavior and have to anticipate what values are valid, or create new tests as bugs are found.

apaprocki 8y ago
Contracts were developed into the C++ standard to make this easier: https://en.cppreference.com/w/cpp/language/attributes/contract https://en.cppreference.com/w/cpp/language/attributes/contra...
fiddlerwoaroof 8y ago
I think in languages like Eiffel that have first-class support for DBC, there’s less noise because the language is designed to propagate contracts appropriately (e.g. making subclasses inherit contracts from their base classes.) Also, there’s been a lot of work in the Racket community on contracts: I think it has something to do with making Racket/Typed Racket interop safe .
throwawayjava 8y ago
There's a whole "paradigm" called "light weight verification". I could point to particular papers, but unfortunately I don't know of a good survey article or exemplar tool/implementation/framework. But the term is very google-able, and skimming papers/tool descriptions will quickly give you a general sense for what sort of things are possible.
macintux 8y ago
It definitely seems like any OOPL would be inherently at a severe disadvantage in this style. In most Erlang code all you’d have to check are the function parameters. One concern I have with their Erlang solution is that the preconditions and postconditions are expressed for the function as a whole, not each function clause. In some contexts, rather like OOP, a function can be quite different depending on the context it’s called with.