philzook

6 ms·

1.
by philzook 1mo ago
A suggestion: I think the python api could be more useful if it returned a structured tree and possibly also could accept a structured tree. I'm guessing you're using maturin, there are some nice low energy ways of getting a tree
2.
by philzook 4mo ago
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 available. I also had some fun modell
3.
by philzook 6mo ago
Interesting. I think there is even more similarity if you are trying to find a "best" list from which two other lists are thinned.
4.
by philzook 8mo ago
https://www.philipzucker.com/ I blog regularly about egraphs, SMT solvers, assembly verification, theorem proving
5.
by philzook 10mo ago
I'm a fan. I've been building a proof assistant directly on the z3py api. https://pypi.org/project/knuckledragger/0.1.3/
6.
by philzook 1y ago
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 pretty happy with. https:/&#x2
7.
by philzook 1y ago
Yeah, using `<=` in this way is pretty sinful. 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 mutually recursively de
8.
Compositional Datalog on SQL: Relational Algebra of the Environment(philipzucker.com)
47 points by philzook 1y ago|3 comments
9.
A Python CLI for Verifying Assembly(philipzucker.com)
1 points by philzook 1y ago|0 comments
10.
by philzook 1y ago
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 the only option though. I had a scam in that post to do sem
11.
by philzook 1y ago
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 syntactically rather than by overload
12.
by philzook 1y ago
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.
13.
by philzook 1y ago
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 = set() for i in range(10): # path
14.
A Python Frozenset Interpretation of Dependent Type Theory(philipzucker.com)
5 points by philzook 1y ago|0 comments
15.
"Verified" "Compilation" of "Python" with Knuckledragger, GCC, and Ghidra(philipzucker.com)
2 points by philzook 1y ago|0 comments
16.
A Small Prolog on the Z3 AST(philipzucker.com)
3 points by philzook 1y ago|0 comments
17.
by philzook 2y ago
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 LLVM. Is your metadata more lightweight,
18.
by philzook 2y ago
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 of rewrite rules for benchm
19.
by philzook 2y ago
This looks great! Are there files or sections in particular I might want to focus on?
20.
by philzook 2y ago
Surely Hacker News has awareness of many, many rewrite rule files. Keep em coming!
21.
by philzook 2y ago
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 engines to equational reasoning / rewriting. I some
22.
by philzook 2y ago
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.
23.
by philzook 2y ago
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 good. It's a good way to learn
24.
by philzook 2y ago
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 interest is due to Tao's recent equation c
25.
by philzook 2y ago
Thank you, this is fascinating advice
26.
by philzook 2y ago
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 impression is that at the single machine l
27.
by philzook 2y ago
It's a good question. I was asking something like this myself at lunch today. Basically I think the issue is that SAT solvers accept stuff at a conjunctive normal form level, which is pretty far from what you'd want to use for mos
28.
by philzook 2y ago
I am also a bit surprised, but happy that people find value here. Maybe just pretend the article ends before "bits and bobbles". Then it is just a short note on a brute force solver and a Davis Putnam solver. I like keeping my not
29.
by philzook 2y ago
This looks like a nice reflection of python into a syntax tree, but unless I'm mistaken, it can't reflect python control structures like if-then-else? Z3 or sympy already are kind of ready to go systems that overload all the typic
30.
by philzook 2y ago
This looks great! The paper linked in your README https://hoheinzollern.files.wordpress.com/2008/04/seer1.pdf also seems like a nice explanation of similar ideas. The reason I'm exploring this idea is to use

More ›