4 ms·

Clojure, with its dabbling in schemas and rule systems / logic programming (as a substitute for conditional statements) and thanks to its great tools (like figw

by ComNik 10y ago

Clojure, with its dabbling in schemas and rule systems / logic programming (as a substitute for conditional statements) and thanks to its great tools (like figwheel or devcards), could really be establishing a cheaper, "as-good" alternative to static typing and full formal verification. Instead of encoding constraints as type signatures, the Clojure folks (true to character) encode them in data. In my eyes a very interesting, pragmatic trade-off between expressiveness and automatic verifiability.

llamaz 10y ago
> dabbling in schemas and rule systems / logic programming (as a substitute for conditional statements That sounds interesting. Could you elaborate or post a link?
- mhluongo 10y ago
  Quick refs to logic programming and pattern matching in Clojure. core.logic https://github.com/clojure/core.logic https://github.com/clojure/core.logic core.match https://github.com/clojure/core.match https://github.com/clojure/core.match
- untothebreach 10y ago
  I assume @ComNik is referring to core.schema and core.logic[1] here, respectively? (if not, sorry @ComNik) 1: https://clojure.github.io/core.logic/ https://clojure.github.io/core.logic/
- ComNik 10y ago
  As a side note in his talk "Simple Made Easy" (https://www.infoq.com/presentations/Simple-Made-Easy https://www.infoq.com/presentations/Simple-Made-Easy, around minute 42) Rich Hickey mentions, that conditional statements are complex, because they spread (business-)logic throughout the program. As a simpler (in the Hickey-sense) alternative, he lists rule systems and logic programming. For example, keeping parts of the business logic ("What do we consider an 'active' user?", "When do we notify a user?", etc...) as datalog expressions, maybe even storing them in a database, specifies them all in a single place. This helps to ensure consistency throughout the program. One could even give access to these specifications to a client, who can then customise the application directly in logic, instead of chasing throughout the whole code base. Basically everyone involved agrees on a common language of predicates explicitly, instead of informally in database queries, UI, application code, etc... But Hickey also notes that this thinking is pretty "cutting-edge" and probably not yet terribly practical.
  - goldbrick 10y ago
    It can work. My current company uses a rule system to represent most of our business logic since it is so dynamic. The downside is that we have to rebuild the entire graph into memory (times the number of threads, times the number of app servers) every time anything changes (which is constant). Facebook wrote about rebuilding a similar system in Haskell that only changes memory incrementally, so it's definitely possible to do better.
    - ComNik 10y ago
      Interesting note, thank you. Are you referring to "Sigma" https://code.facebook.com/posts/745068642270222/fighting-spam-with-haskell/ https://code.facebook.com/posts/745068642270222/fighting-spa... ?
      - goldbrick 10y ago
        That's the one.
ohpauleez 10y ago
Important to note, that as data, they can be consumed by other systems for other purposes. For example, it's feasible to consume a spec within Alloy and use a SAT solver (which is made even easier given the split on keyset). This pushes spec from design and requirements validation, into runtime constraints, and on through to tests and verification.
pklausler 10y ago
Cheaper? How so?
- ComNik 10y ago
  Full, formal verification of complex systems (especially in the distributed case) requires a lot of modelling effort, beyond what is needed for "mere" implementation. A lot of important constraints cannot even be expressed in most type systems. And if one uses a specialised modelling language for the proof, the actual implementation might introduce bugs. Also relevant to real, shipping software: specifying a program in such that detail as required for automatic verification makes it even harder to change (which, given infinite time and money, is indeed a very very good property!). This just goes to say, that a type system can be very helpful, but is ultimately just a part of regular testing. So for most companies and most developers, anything that aides in keeping documentation up-to-date, writing or generating tests and helping developers understand what they are reading is probably a better ROI.
  - pklausler 10y ago
    If static type systems cannot do everything, it does not make sense to me to conclude that they shouldn't then be used for anything. Type systems aren't part of "regular testing", they're part of compile-time error checking.
    - ComNik 10y ago
      That was not the intension behind my comment at all. I rely on type systems a lot, myself. I was trying to note that Clojure, as a dynamic language, is making a (to my eyes) very interesting choice, of doubling down on these dynamic methods of verification. For some uses, I can see this as the better choice, for others it isn't and won't be.
      - pklausler 10y ago
        Sure, and I can't fault anyone for wanting less dangerous dynamic languages. But to me it's kind of like wanting less dangerous cigarettes.
aconz2 10y ago
> Instead of encoding constraints as type signatures, the Clojure folks (true to character) encode them in data. I've never bought this line of thinking when the "Clojure folks" also say "code is data", because then a syntactic type signature you write down is also just data. If you want to consume the type signature (or spec signature or whatever) as syntax (as a sibling comment suggests), use a macro or any other program which consumes programs. The thing I do see as being important is not how you write these things down, but whether they have an accessible representation at run/read/compile/whenever time. Lastly, I strongly disagree these approaches are meant as a replacement for static typing or formal verification because (as far as I can tell) a value can be checked against a spec on demand, but makes zero guarantees as to what that value does in other parts of a program. This is also in contrast to Racket contracts, which will give you the correct blame information between parties using and not using contracts.
- ComNik 10y ago
  You make a very good point, the comparison was flawed there. > The thing I do see as being important is not how you write these things down, but whether they have an accessible representation at run/read/compile/whenever time. This is a better way to put it. The second important factor for me is expressiveness. With spec or any other contracts-like system one gets the full power of the language to express constraints. Of course type systems are not artificially restricted in this regard, they simply make a different trade-off. I hope my comment did not come off as a riff on static vs dynamic typing, and I don't think any contract system is meant to replace type systems. Until expressing all important program specifications formally becomes viable for everyone (maybe through this work https://www.math.ias.edu/vladimir/current_work? https://www.math.ias.edu/vladimir/current_work?), a less-formal, dynamic approach seems very attractive.
  - aconz2 10y ago
    I hear you on expressiveness of using the language. Of course (and as you mention) the strength of restricting the expressiveness is that it becomes decidable in some amount of acceptable time for most programs. I agree with your last sentiment but I don't think it has to be any less "formal" than something like Coq. I just think we shouldn't be so concerned with proving all properties of a program before running. And then we can turn the knob to adjust how much to prove during vs. before running.

by ComNik 10y ago

llamaz 10y ago

> dabbling in schemas and rule systems / logic programming (as a substitute for conditional statements That sounds interesting. Could you elaborate or post a link?

mhluongo 10y ago
Quick refs to logic programming and pattern matching in Clojure. core.logic https://github.com/clojure/core.logic https://github.com/clojure/core.logic core.match https://github.com/clojure/core.match https://github.com/clojure/core.match
untothebreach 10y ago
I assume @ComNik is referring to core.schema and core.logic[1] here, respectively? (if not, sorry @ComNik) 1: https://clojure.github.io/core.logic/ https://clojure.github.io/core.logic/
ComNik 10y ago
As a side note in his talk "Simple Made Easy" (https://www.infoq.com/presentations/Simple-Made-Easy https://www.infoq.com/presentations/Simple-Made-Easy, around minute 42) Rich Hickey mentions, that conditional statements are complex, because they spread (business-)logic throughout the program. As a simpler (in the Hickey-sense) alternative, he lists rule systems and logic programming. For example, keeping parts of the business logic ("What do we consider an 'active' user?", "When do we notify a user?", etc...) as datalog expressions, maybe even storing them in a database, specifies them all in a single place. This helps to ensure consistency throughout the program. One could even give access to these specifications to a client, who can then customise the application directly in logic, instead of chasing throughout the whole code base. Basically everyone involved agrees on a common language of predicates explicitly, instead of informally in database queries, UI, application code, etc... But Hickey also notes that this thinking is pretty "cutting-edge" and probably not yet terribly practical.
- goldbrick 10y ago
  It can work. My current company uses a rule system to represent most of our business logic since it is so dynamic. The downside is that we have to rebuild the entire graph into memory (times the number of threads, times the number of app servers) every time anything changes (which is constant). Facebook wrote about rebuilding a similar system in Haskell that only changes memory incrementally, so it's definitely possible to do better.
  - ComNik 10y ago
    Interesting note, thank you. Are you referring to "Sigma" https://code.facebook.com/posts/745068642270222/fighting-spam-with-haskell/ https://code.facebook.com/posts/745068642270222/fighting-spa... ?
    - goldbrick 10y ago
      That's the one.

ohpauleez 10y ago

Important to note, that as data, they can be consumed by other systems for other purposes. For example, it's feasible to consume a spec within Alloy and use a SAT solver (which is made even easier given the split on keyset). This pushes spec from design and requirements validation, into runtime constraints, and on through to tests and verification.

pklausler 10y ago

Cheaper? How so?

ComNik 10y ago
Full, formal verification of complex systems (especially in the distributed case) requires a lot of modelling effort, beyond what is needed for "mere" implementation. A lot of important constraints cannot even be expressed in most type systems. And if one uses a specialised modelling language for the proof, the actual implementation might introduce bugs. Also relevant to real, shipping software: specifying a program in such that detail as required for automatic verification makes it even harder to change (which, given infinite time and money, is indeed a very very good property!). This just goes to say, that a type system can be very helpful, but is ultimately just a part of regular testing. So for most companies and most developers, anything that aides in keeping documentation up-to-date, writing or generating tests and helping developers understand what they are reading is probably a better ROI.
- pklausler 10y ago
  If static type systems cannot do everything, it does not make sense to me to conclude that they shouldn't then be used for anything. Type systems aren't part of "regular testing", they're part of compile-time error checking.
  - ComNik 10y ago
    That was not the intension behind my comment at all. I rely on type systems a lot, myself. I was trying to note that Clojure, as a dynamic language, is making a (to my eyes) very interesting choice, of doubling down on these dynamic methods of verification. For some uses, I can see this as the better choice, for others it isn't and won't be.
    - pklausler 10y ago
      Sure, and I can't fault anyone for wanting less dangerous dynamic languages. But to me it's kind of like wanting less dangerous cigarettes.

aconz2 10y ago

> Instead of encoding constraints as type signatures, the Clojure folks (true to character) encode them in data. I've never bought this line of thinking when the "Clojure folks" also say "code is data", because then a syntactic type signature you write down is also just data. If you want to consume the type signature (or spec signature or whatever) as syntax (as a sibling comment suggests), use a macro or any other program which consumes programs. The thing I do see as being important is not how you write these things down, but whether they have an accessible representation at run/read/compile/whenever time. Lastly, I strongly disagree these approaches are meant as a replacement for static typing or formal verification because (as far as I can tell) a value can be checked against a spec on demand, but makes zero guarantees as to what that value does in other parts of a program. This is also in contrast to Racket contracts, which will give you the correct blame information between parties using and not using contracts.

ComNik 10y ago
You make a very good point, the comparison was flawed there. > The thing I do see as being important is not how you write these things down, but whether they have an accessible representation at run/read/compile/whenever time. This is a better way to put it. The second important factor for me is expressiveness. With spec or any other contracts-like system one gets the full power of the language to express constraints. Of course type systems are not artificially restricted in this regard, they simply make a different trade-off. I hope my comment did not come off as a riff on static vs dynamic typing, and I don't think any contract system is meant to replace type systems. Until expressing all important program specifications formally becomes viable for everyone (maybe through this work https://www.math.ias.edu/vladimir/current_work? https://www.math.ias.edu/vladimir/current_work?), a less-formal, dynamic approach seems very attractive.
- aconz2 10y ago
  I hear you on expressiveness of using the language. Of course (and as you mention) the strength of restricting the expressiveness is that it becomes decidable in some amount of acceptable time for most programs. I agree with your last sentiment but I don't think it has to be any less "formal" than something like Coq. I just think we shouldn't be so concerned with proving all properties of a program before running. And then we can turn the knob to adjust how much to prove during vs. before running.