Viewing profile — philzook

It's a really neat board. You can get kits from aliexpress etc. I wrote up some notes here https://www.philipzucker.com/td4-4bit-cpu/ . English descriptions are not so readily avai…

Interesting. I think there is even more similarity if you are trying to find a "best" list from which two other lists are thinned.

https://www.philipzucker.com/ I blog regularly about egraphs, SMT solvers, assembly verification, theorem proving

I'm a fan. I've been building a proof assistant directly on the z3py api. https://pypi.org/project/knuckledragger/0.1.3/

I'm working on Knuckledragger, a proof assistant shallowly based upon z3py https://github.com/philzook58/knuckledragger Yesterday I proved the infinitude of primes, which I was pre…

Yeah, using ` My maybe inaccurate understanding of recursive CTEs was that they only allow linear occurrences of the recursively defined relation in the query and do not allow many…

My suspicion is that if you can get away with it that recursive CTEs would be more performant than doing the datalog iteration query by query. AFAIK for general rules the latter is…

Love it! I was trying to use python as a dsl frontend to Z3 in a different way https://github.com/philzook58/knuckledragger/blob/ecac7a568a... (it probably has to be done syntactic…

Thanks! I wouldn't so much say it was written so much as it was vomited out in a year of enthusiasm, but I'm glad it has some value.

Nice! I'll note there is a really shallow version of naive datalog I rather like if you're willing to compromise on syntax and nonlinear variable use. edge = {(1,2), (2,3)} path = …

What is the distinction between this approach and Address Sanitizer https://clang.llvm.org/docs/AddressSanitizer.html ? If I understand correctly, Fil-C is a modified version of LL…

Wide context. But to be a bit more specific, I've been involved in the egraphs community https://github.com/philzook58/awesome-egraphs and we don't currently have a shared database…

This looks great! Are there files or sections in particular I might want to focus on?

Surely Hacker News has awareness of many, many rewrite rule files. Keep em coming!

I don't always care about consistency between rule sets. Depends what I'm trying to do. The question at hand is motivating and getting benchmarks for different approaches or engine…

I'm curious if there is a useful connection between Apache's rule and other term rewriting. Some sort of static analysis? If there is a interesting database of them, I'd add it.

Just celebrated my 10 year anniversary https://www.philipzucker.com/ten_year_blog/ actually. It has not generated new jobs for me, but I haven't been looking really. Writing is goo…

It's interesting how sometimes it feels like a topic starts showing up super often all of the sudden. It probably isn't a coincidence, since my interest and probably this post's in…

Thank you, this is fascinating advice

https://github.com/domschrei/mallob I've seen talks by AWS where they claim that distributed SAT solving is very effective. Do you need it to be parallel or just fast? My impressio…