philzook

20 ms·

1. 211.▲
   by philzook 7y ago

   http://www.philipzucker.com/ Functional programming, formal methods, category theory, physics, robotics, control I like to blog little implementations of interesting ideas and explanations. Trying to make the abstract concr
2. 212.▲
   Computational Category Theory in Python I: Dictionaries for FinSet (2020)(philipzucker.com)

   2 points by philzook 7y ago|0 comments
3. 213.▲
   by philzook 7y ago

   You can achieve a certain amount of type disequality in Haskell. It isn't necessarily easy or sufficient for all purposes. There is a type family that returns a type level Bool for equality here. https://hackage.haskell.org&
4. 214.▲
   by philzook 7y ago

   Wow, this is a common theme. I have a 2015 13" macbook which wasn't max specced out and I feel like I'm hurting these days RAM wise and HardDrive wise. I bought a super specced out 2020 XPS 13 2 in 1 because of reservations a
5. 215.▲
   by philzook 7y ago

   Looks really good!
6. 216.▲
   Categorical Combinators for Convex Optimization (2020)(philipzucker.com)

   1 points by philzook 7y ago|0 comments
7. 217.▲
   Categorical Combinators for GraphViz in Python (2020)(philipzucker.com)

   2 points by philzook 7y ago|0 comments
8. 218.▲
   by philzook 7y ago

   I love MIP. It's super useful. I like to think that MIP is a framework that meets halfway between a natural modeling language and a natural solution language. The reason it's good is that the framework naturally lends itself to ab
9. 219.▲
   by philzook 7y ago

   I wonder to what degree dimensional analysis and free theorems are connected. The rabbit out of the hat style reasoning feels very similar to me. I suppose one could use polymorphic type variables as units with the appropriate definitions o
10. 220.▲
    by philzook 7y ago

    Very cool! Ever looked at the Viper project? It's the only other system in python that I know of targeting pre and post conditions https://www.pm.inf.ethz.ch/research/viper.html https://www.pm.inf.ethz.
11. 221.▲
    by philzook 7y ago

    Seems up to me.
12. 222.▲
    Verifying a Keras Neural Network with Z3 (2019)(philipzucker.com)

    1 points by philzook 7y ago|0 comments
13. 223.▲
    by philzook 7y ago

    This is absolutely nuts! Congrats!
14. 224.▲
    by philzook 7y ago

    Yes, thanks for this. It appears that maybe the entire university's website has changed location? So maybe a more official link will come back up soon
15. 225.▲
    by philzook 7y ago

    I think I've got the category bug. I very much was intrigued by Milewski's course and found that it made things happening in Haskell make more sense to me. There are a couple of things that really excited me. Conal Elliott's
16. 226.▲
    by philzook 7y ago

    Check out Program Design by Calculation and The Algebra of Programming. Category theory and related formalisms do have a strong case to being a formal theory for designing/calculating programs http://www4.di.uminho.pt/~
17. 227.▲
    by philzook 7y ago

    And Conal Elliott's Compiling to Categories, which I've seen discussed here before http://conal.net/papers/compiling-to-categories/
18. 228.▲
    by philzook 7y ago

    People who like this may also be interested in the awesome applied category theory list https://github.com/statebox/awesome-applied-ct
19. 229.▲
    by philzook 7y ago

    Being into functional programming helps quite a bit I think. In particular, category theory seems to nest well and illuminate some complicated uses of polymorphism and continuation passing style transformations. Categories are also a useful
20. 230.▲
    Verifying Sorting Networks Off of Wikipedia (2019)(philipzucker.com)

    1 points by philzook 7y ago|0 comments
21. 231.▲
    by philzook 7y ago

    But also things that aren't radiation or high energy physics. Inverse square laws are ubiquitous in hydrodynamics, heat flow, electrostatics. Good ole fashioned 19th century physics. And I think that's its most natural arena.
22. 232.▲
    by philzook 7y ago

    An interesting but rather overcomplicated seeming explanation. The posted article basically is saying inverse square laws results from conversation of flux (of any kind) in 3d. That seems like a pretty good explanation to me
23. 233.▲
    Categorical LQR Control with Linear Relations (2019)(philipzucker.com)

    1 points by philzook 7y ago|0 comments
24. 234.▲
    by philzook 7y ago

    I've heard a completely unverified, probably untrue story that it is the French's revenge for the word "bit", which translates crudely.
25. 235.▲
    by philzook 7y ago

    It is fun and useful if you're interested in formal program correctness or mathematics. Maybe it's a useful bitter pill to swallow even if you're not, but the world is a wide and wonderful place, and maybe Coq isn't the
26. 236.▲
    by philzook 7y ago

    Short and informal is hard to come by here, especially by such a formal system built by such formal people. This tutorial maybe? https://coq.inria.fr/tutorial-nahas This particular chapter of Software Foundations may be hel
27. 237.▲
    by philzook 7y ago

    You may be interested in a recent survey "QED at Large: A Survey of Engineering of Formally Verified Software" https://www.nowpublishers.com/article/Details/PGL-045 (have to sign up for a free account to
28. 238.▲
    by philzook 7y ago

    As a side note, I believe native floating point operations are in the works. This is more of a speed benefit though? http://drops.dagstuhl.de/opus/volltexte/2019/11062/pdf/LIPIc...
29. 239.▲
    by philzook 7y ago

    As others have mentioned, it's possible and has been done in the FlocQ library. I don't have personal experience using them. I would expect proving properties to be somewhat challenging. There is a book available https:/&#x2
30. 240.▲
    by philzook 7y ago

    Hey neat! I wrote this tutorial. Lemme know if you have suggestions for improvement (or you can make a pull request).