syrak

10 ms·

1.
Creusot 0.11.0: VerifyThis Winner(devlog.creusot.rs)
1 points by syrak 5mo ago|0 comments
2.
Creusot: Devlog(creusot-rs.github.io)
2 points by syrak 9mo ago|0 comments
3.
by syrak 1y ago
You need very little to make a Prolog-like language Turing-complete (lists and recursive predicates). And so Haskell's type system only needs one (or two) extensions to be Turing-complete, `UndecidableInstances` (and maybe `FlexibleIns
4.
by syrak 2y ago
I learned a lot from this and your other comment here! The way I connected the dots when I read about Clear (and OBJ) is that it let me explain free algebras by example, by just showing Clear code. That hopefully makes the concept more acce
5.
by syrak 2y ago
IMO your view, if not common, is kinda intuitive from the point of view of someone trained in set theory/classical logic (i.e., most people before they find an interest in type theory; I myself was here a few years ago). If it feels li
6.
by syrak 2y ago
Thanks for sharing this! These tidbits of history are fascinating.
7.
by syrak 2y ago
Thanks! Here we go: "Note: In versions of Miranda before release two (1989) it was possible to associate "laws" with the constructors of an algebraic type, which are applied whenever an object of the type is built. For detail
8.
by syrak 2y ago
That's surprising! I (author of the blog) just repeated what's in the 1985 paper. The feature might actually have been removed, or never even been implemented. One would have to find an implementation to check.
9.
by syrak 2y ago
Is that something he did to people who mis-cited his language?!
10.
by syrak 2y ago
Author here. It's funny you mention this. I was (am still) writing a post about it, and I went on a rant that while it's a (fun!) way to do "algebra with types", it's not actually the original meaning of it afaik, a
11.
by syrak 2y ago
That point is discussed in the paper: circle-freeness is Pi^0_2 in the arithmetic hierarchy, so there isn't a reduction to halting (Sigma^0_1) in the usual sense of a mapping between inputs. And in fact, Turing's paper does do a c
12.
by syrak 2y ago
The paper in the OP discusses this claim in section 3, and mentions that Kleene came even before that: > We would note that Kleene seems, however, to have already had the self-referential argument earlier in his classic book from 1952, I
13.
by syrak 2y ago
For verified Rust there is also https://github.com/creusot-rs/creusot
14.
by syrak 3y ago
The write up is pretty nice https://sugawarayuuta.github.io/charcoal/ Since that's the point of comparison, what's the Go standard library's strategy? Is it inherently slower than this or does it behave
15.
by syrak 3y ago
This post is rendered at https://sugawarayuuta.github.io/charcoal/
16.
Ffs: The File Fileystem(mgree.github.io)
4 points by syrak 5y ago|1 comments
17.
by syrak 5y ago
Even if you had a verified SMT checker, you also need to prove that the encoding of the problem in SMT is correct, i.e., that a proof does translate to a valid register allocation solution, to achieve comparable guarantees to CompCert.
18.
by syrak 6y ago
I've learned quite a lot about editing from "Style: Lessons in Clarity and Grace." It presents some tricks to restructure and improve the flow of sentences, and through that process, to generate the momentum to really think a
19.
by syrak 7y ago
> If the underlying premise is flawed, who cares if the methodology is correct? How do we know the premise is flawed? > The first step should be to show that the github dataset can be used to say anything about quality and productivit
20.
by syrak 7y ago
> It's not clear to me that it has any use at all if you don't have higher-order functions. The very origin of defunctionalization is to emulate higher-order functions in a language without them. https://en.wikipedia
21.
by syrak 7y ago
O(N + M) is not equivalent to O(N) if you make no assumptions about the relative growths of N and M, that's why it's actually meaningful to keep both terms around. You can only reduce it to O(N) when N dominates M (M = O(N)).
22.
by syrak 7y ago
> I do wonder why people keep building more systems of this kind. Not a lot of languages have higher-inductive types which is the main advertised feature here. At least they're missing in Isabelle and Coq. That's also orthogona
23.
by syrak 7y ago
> I've never read a code base where I thought the type system was doing a good job of being a DSL for describing business requirements Would refinement types help in that respect? For example, the F* language. https://www
24.
by syrak 7y ago
> In this case it is hard to be sure that the function must behave in the correct way because of its type. I would argue that in this case it is quite easy to ensure that it does the right thing, because even if the implementation is not
25.
by syrak 7y ago
This is an interesting question. Technically there is more than one possible implementation, but you would also have to go out of your way to get it wrong. Automatically determining what constitutes "going out of your way" so that
26.
by syrak 8y ago
Hello there. I'm the author of this repo. Not as much has been going on in that project as I would have liked. It certainly doesn't help that: - The standard library is actually quite poor. A lot of basic functions must be impleme
27.
by syrak 8y ago
The Coq compiler is unverified, it is written in OCaml. It's not possible for Coq's consistency to be verified in itself, thanks to Gödel's second incompleteness theorem. However there are still various other aspects of the c
28.
by syrak 8y ago
It does not.
29.
by syrak 8y ago
aurman. More choices can be found here https://wiki.archlinux.org/index.php/AUR_helpers
30.
by syrak 9y ago
What's fascist is to forbid people from having children based on arbitrary criteria, which is just one obvious but wrong way to address an otherwise reasonable idea, that not everyone is fit for parenting. It doesn't mean the idea

More ›