c-cube

35 ms·

391.
by c-cube 9y ago
Just to give credit where it's due, I believe why3 is developed purely by LRI, a public french research lab (see http://why3.lri.fr/ ). It's indeed used as a proof backend in several tools, including frama-C and Da
392.
by c-cube 9y ago
Agreed, some things are still missing (in particular my pet peeve, iterators; also unicode strings). But for what it provides, OCaml's stdlib is reasonably well designed and performs well.
393.
by c-cube 9y ago
Sets don't need to be native in languages that are both fast and have a proper type system. For example, rust and OCaml have a standard set in their stdlib, but it's not builtin. Of course, go lacking generics makes it impossible
394.
by c-cube 9y ago
Nowadays, OCaml has so many more syntactic sugar and typing goodies compared to SML, that it's not fair to compare them anymore. I'm no expert in SML, but from what I know: - OCaml's pattern matching is more powerful (more or
395.
by c-cube 9y ago
So, not even referencing the decades of research in the field of ATP? :/
396.
by c-cube 9y ago
As a programmer, I consider a format that is deeply tied to one particular editor as "don't touch it with a 10 foot pole". Org-mode without emacs isn't particularly attractive (I prefer markdown or asciidoc when it comes
397.
by c-cube 9y ago
So, there are two main areas of development in the automation of theorem proving. The first one is proof assistants, such as Isabelle/HOL, HOL Light, HOL4, Coq, PVS, Lean, TLApm (and others). These are typically languages to be used di
398.
by c-cube 9y ago
> I believe that there will eventually be something like a smart safe city where 2000+ pounds vehicles to not freely mix with pedestrians, cyclists, and baby strollers. I think it's called Amsterdam ;-) More seriously, I went there
399.
by c-cube 9y ago
That's more a proof that the grammar of C++ is absolutely terrible. More modern languages such as rust have been carefully designed to be parsable by non-necronomicon-level code.
400.
by c-cube 9y ago
I think most of the enumeration-based synthesis tools rely on a SMT solver (Z3 or CVC4, say) to learn from bad solutions.
401.
by c-cube 9y ago
I don't think so. I'm not really competent to say if the NLP part will be solved soon, but (fully) automated theorem proving is very hard, and I don't see deep learning applying to it very well. What could happen, though (hop
402.
by c-cube 9y ago
Author here. The implementation is quite straightforward (both for the bottom-up seminaive fixpoint, and for the top-down full prolog with tabling). Good generalist in-memory implementations would be, afaik, [XSB Prolog]( http://x
403.
by c-cube 10y ago
you can start by looking for "warren abstract machine" (usually shortened as WAM). It's an intermediate format for compiling prolog programs (sets of Horn clauses, that is, rules). It makes every operation very explicit, incl
404.
by c-cube 10y ago
There are some automated theorem provers for higher-order logic [0][1], but they are not very good yet compared to their first-order counterpart. There are also some provers specialized in inductive proofs [2][3], although the frontier with