pschanely

> I believe your argument on the performance penalty is right, and as a corollary, this implies that contracts are mostly useful if associated with a formal proof system. Contracts in production are probably a bad idea, in most cases.

Agree! There is a sliding scale between testing contracts and proving them too. My labor of love for the past several years has been a tool for checking Python contracts using an SMT solver (using symbolic inputs over concrete paths): https://github.com/pschanely/CrossHair

That said, these days I think property-based testing gets you the ~same benefits as contracts, and is easier for most people to apply.

A little encouragement goes such a long way. Thank you for trying it out, and especially for coming back here to let me know how it went!

Oh, thank you! I don't have any plans for expanding to other music services. But skimming the Apple Music API, I think it's possible. Particularly if you think you'd use it, I'll investigate a bit more and let you know. :)

Music Tonight: https://musictonightapp.com/

Makes a Spotify playlist of artists playing near you, tonight.

No revenue. I really just made it for me; make the playlist in the am, listen during the day, and maybe see something that night.

Great! Sadly, I don't see anything on linkedin though. Feel free to just ping me by email: [email protected]

Sadly, mine largely aren't committed to words yet. I do have a small thing on implementing regular expressions: https://medium.com/@pschanely/modeling-python-regular-expres...

But there is so much to talk about: gotchas with quantifiers, mixing logics, multiplication, float conversions. I'll try to write up some more of my experiences if that's valuable for folks!

Looking at some of your SMT-based projects, I'd love to compare your SMT solver notes with my mine from working on https://github.com/pschanely/CrossHair

Sadly, there aren't a lot of resources on how to use SMT solvers well.

Totally agree that this is confusing. I've stolen and committed your suggestion. Thank you both!

Yes. Z3 is impressive. I intend to do a write-up of how I chose to model Python values in it soon.

That's right! We pick different choose execution paths arbitrarily and accumulate constraints in an SMT solver as we go. It's implemented with special objects that look just like ints, strings, etc; this might help:

https://twitter.com/pschanely/status/1176151748844691456

That would be amazing. It's easy to turn CrossHair into an absurdly slow fuzz tester (imagine hashing or printing your inputs early in the process). I think the ideal product would be good at both symbolic and concrete tactics, and the minimization logic of hypothesis would be really nice to have too. I will be in touch!

Hi all! My primary objective with this post is to find potential collaborators and people willing to try it. (and file bugs!)

If you do try it, I'd encourage you to think of it as an exercise in formally documenting your code's behavior, with the side benefit that CrossHair can sometimes help you ensure the correctness of that documentation.

And, of course, feedback of any kind at all is honestly appreciated. Thanks for being the awesome community that you are!

The README.md goes fast, but I have some feel for what's going on. Could I, for instance, connect a client and start logging every message in the system using a liberal matcher and a low weight? Also, it's not obvious to me how the versions work. Can I use a transformer to "upgrade" an older message version to a newer one?

I'm glad that other folks think this is important too.

Stay tuned on twitter/medium. That python library also supports a viewabledict (for key-value mappings). I've got an experimental compiler which starts with an AST (stored as a tree of these maps), and then chains type checking and code generation off that to make incrementally updating binaries. Just supporting a toy language to start, but it will make a nice demo I think!

Referenced in the paper panic suggested below ( https://news.ycombinator.com/item?id=11595273 ), and suggested to me directly by @mattcmd on twitter ( https://twitter.com/mattmcd/status/726342652845809664 ), there is something called the "fusion property of fold," which would explain transformations I'm discussing here applied to folds (sided reduce). From the paper ( http://www.cs.nott.ac.uk/~pszgmh/fold.pdf ), (and some minimal editorial substitution from me) we see that:

h(fold(g, w, l)) = fold(f, h(w), l)

if

h(g(x, y)) = f(x, h(y))

This is exciting because (1) it suggests the equivalent transformation for sided reduces (folds), and (2) fold is a more general operator than the others. My somewhat silly use of "hypothetical inverses" effectively just creates a goalpost to (1) constructively find the the function f, given g (or vice-versa) and (2) prove the necessary condition.

Very exciting.

Yes! I think perhaps that f needs only to be a homomorphism instead of an isomorphism, but I don't trust myself enough to make such a claim definitively :)

Always curious to follow people doing compiler work; loop me in, yeah?

And, just watched that Wadler talk; it's good stuff. Of course, it sounds like his scenario is like: "there is a way to do the transformation, you just have to find it," and in my case, it's more like: "there might or might not be an algebra in which f acts as a homomorphism, and, even if there is, you may not have the transformations you need to determine it!"

Unfortunately, I took barely enough grad school classes to be dangerous! It's worth clarifying that the lifting of f through r can change r (to, say r'), in which case, yes, f is a homomorphism from an algebra with r' to an algebra with r. (hopefully I got that right?)

I am curious about the idea that the inputs and outputs of r may not need to be of the same type, and want to investigate further (help is appreciated!). Since r is given to reduce(), at least one of its inputs must match its output, depending on how you define reduce(). Haskell's fold(l/r) permit the non-accumulator side to differ in type from the output, but the output must match the accumulator side. I think some similar transformation may apply to folds, but haven't thought about it enough.

Thank you. And, heck yes, more people need to be talking about how to deal with computations that are largely repeated. That problem comes up all over the place.

Couchdb had an interesting approach for this that did not require inverses: they persist intermediate reduce results, so that you can re-use nodes in the tree that haven't changed. So clever. http://horicky.blogspot.com/2008/10/couchdb-implementation.h...

Great observations. For the purposes of this exploration, I am entirely assuming arbitrary precision integers (and the math geek in me is really enjoying your use of the adjective "junk", above).

Bigger picture, I want to rewrite "sum(reverse(x))" without explicitly saying so. How do we optimize that expression using the definitions of sum and reverse? Note that in my discussion of this in my second example, I am inconsistent here: I expand the definition of reverse() but treat sum() as a primitive. That said, I am pretty sure that the example still works if you substitute the appropriate definition of sum as "reduce(add,x)"; the derivation is just longer.

Totally; great point. My code is here: https://github.com/pschanely/wf-optimizer/blob/master/demo.m...

Maude is a programming language based on rewriting: http://maude.cs.illinois.edu/w/index.php

It's pretty wild; your code doesn't "execute" in the traditional sense; instead patterns match the code and transform it repeatedly until it reaches a "normal form" - one that cannot be rewritten further.

Maude is handy for playing with optimizers, because you very often want to specify behavior in terms of patterns (when you see these functions together, replace them with this...)

Thanks! I have a link to code written in Maude at the very bottom; The code needs so much explanation though. Perhaps I'll highlight the code link at the top of the article?

Ah, I knew that HN would tell me what I should be reading! I've only been able to spend a few minutes reading this one, but it looks to me like the first focus there is on eliminating intermediate containing structures, with some interesting opportunities for optimization afterwards. Their stream definition of fold(l/r) is still recursive, so I don't think it would be able to pull, for example, the incr() outside the reduce in my first example of "reduce(max, map(incr, l))" I think the approaches might be complimentary, actually; you might apply the higher level transformations I describe first and use a stream approach to implement the resulting chain of operations. Going to need to do a deeper investigation later today, but, anything else I should be looking at?