philzook

18 ms·

151.
by philzook 6y ago
dune, opam, VS Code Ocaml Platform are pretty solid trifecta tooling wise. dune confuses me, but what build tool doesn't? Library-wise we use bap and core as our main things. The documentation of both is rather hard to traverse through
152.
Progress on Automated Reasoning for Catlab with Metatheory.jl Egraphs(philipzucker.com)
1 points by philzook 6y ago|0 comments
153.
by philzook 6y ago
I love it. It's brilliant to side step the whole issue of how to get access to pixels on your screen or in a png, which in some instances is an awful afternoon of frustration. It's almost always easy to get printing going.
154.
by philzook 6y ago
Those are gorgeous. How were they done? Using Julia packages?
155.
by philzook 6y ago
It's a question I hadn't really considered before. On first pass, as far as I know, I'd say the answer is no. It isn't clear to me what the objective of embedding Coq with a C api for example would be. The very core of C
156.
by philzook 6y ago
I do agree that they are usually not mentioned as competitors. Z3 does indeed basically find things, and Coq does mostly just verify things and not find them for you.
157.
by philzook 6y ago
Coq is usually called an interactive theorem prover, not an automated prover. Interactive provers tend to accumulate varying degrees of automation. Coq is a project at the scale of other niche programming languages. It is more of a platform
158.
by philzook 6y ago
They actually have different enough use cases and abilities that it is rare to consider them as competitors. The logic of Coq is vastly more expressive and it's proof process is vastly more controllable. All of this comes at the cost o
159.
Translating My Z3 Tutorial to Coq(philipzucker.com)
108 points by philzook 6y ago|18 comments
160.
CEGARing Exponentials into Z3 with Intervals and Python Coroutines(philipzucker.com)
1 points by philzook 6y ago|0 comments
161.
by philzook 6y ago
Thanks!
162.
by philzook 6y ago
"Set theory" can mean different things. The looser interpretation of set theory is just using the intuitive notion of sets to model things. I think basically everyone is for that and learning these topics is definitely the lower
163.
Z3, the Word Problem, and Path Homotopy as Equality(philipzucker.com)
3 points by philzook 6y ago|0 comments
164.
Automated Propositional Sequent Proofs in the Browser with Tau Prolog(philipzucker.com)
33 points by philzook 6y ago|3 comments
165.
by philzook 6y ago
These are other good resources: - rise4fun https://rise4fun.com/z3/tutorialcontent/guide - https://ericpony.github.io/z3py-tutorial/guide-examples.htm - Programming Z3 - https://the
166.
by philzook 6y ago
I'm giving a tutorial in a couple of days. Vids will be up later. https://github.com/philzook58/z3_tutorial
167.
Developing Mathematical Software in C(fredrikj.net)
5 points by philzook 6y ago|2 comments
168.
Sketchy Exact Reals from Interval Arithmetic (2021)(philipzucker.com)
2 points by philzook 6y ago|0 comments
169.
Weakest Precondition with Z3Py(philipzucker.com)
1 points by philzook 6y ago|0 comments
170.
by philzook 6y ago
I'm on board for there being a problem with conflating programming languages with things that are not. This was a revelation for me for example with Verilog, which almost has the trappings of an ordinary programming language but is not
171.
by philzook 6y ago
Thanks! If there is an utility to this post other than just as an exercise in using Z3Py, it isn't just getting TLA+ into Z3 which as you say is already covered by the apalache project. I think that as someone who doesn't really k
172.
Modeling TLA+ in Z3Py(philipzucker.com)
34 points by philzook 6y ago|9 comments
173.
by philzook 6y ago
I don't think you necessarily need much scheme knowledge to start learning minikanren. You might in order to read the implementation. There are versions out there in most languages I'd suggest just poking around in these first: h
174.
by philzook 6y ago
Two fun blogs posts in this vein https://bentnib.org/posts/2015-04-17-propositions-as-filenam... http://conal.net/blog/posts/the-c-language-is-purely-functio...
175.
by philzook 6y ago
The most important thing about blogging is to just get started and make it low energy. However, I was using wordpress for ~5 years and it was rotting under my feet. It served really slow. I also feel much more secure not having my content i
176.
by philzook 6y ago
The linked tweet is to a slightly more recent rendition of the course (spring 2020 I think). It doesn't appear to be linked from the ocw.mit.edu web page yet. I don't see RISC-V in the syllabus of your linked 2017 version, but I m
177.
by philzook 6y ago
A fun post. I liked seeing some things I knew summarized and some things I didn't know. It is fascinating to me that functional programming techniques and object oriented techniques become intersecting once you know enough about the tw
178.
Dataframes.jl Style Linear Relations(philipzucker.com)
1 points by philzook 6y ago|0 comments
179.
by philzook 6y ago
The SMT-COMP competition is held every year. https://smt-comp.github.io/2020/results.html Look up your problem domain and see how they compare. A nice thing about the smtlib2 format is that you can try the same proble
180.
Executing Categories(philipzucker.com)
1 points by philzook 6y ago|0 comments

More ›