syrak

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 `FlexibleInstances` or `MultiParamTypeClasses`). It is no accident. The name "undecidable" shows that the authors of that extension were well aware that it enables Turing-completeness.

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 accessible than the dry mathy definitions that would have the eyes of most readers glaze over.

I must say that I'm not familiar with Burstall and Goguen's line of research beyond what I've written so far. In the future I'd especially like to know what lessons these specification languages can teach (or already taught) about ML-style module systems, OO languages, and formalizations of mathematical structures in proof assistants (Clear reminds me of the little I've seen of Hierarchy Builder in Coq).

One concrete question I have is how Clear or OBJ or Maude code is actually meant to be run. Your description of these languages reminds me of model checking tools like TLA+/Alloy. Does Maude target a similar niche?

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 like you're in a minority, it's because most others who might have the same opinion haven't reached the point where they could articulate it; many just give up way earlier on understanding type theory.

It certainly makes sense to a set theorist that union and intersection are more primitive than sums and products. From that perspective, type theory seems like a roundabout and unnecessary way of doing things.

The challenge is to imagine type theory as a radically different foundation to logic (because that's what it is), with sums and products as primitives instead, for one superficial difference.

It's hard to explain in words. I personally didn't get it without years of first-hand experience with proof assistants based on type theory. Constructivism and category theory are other possible gateways into the right mindset.

There is one key difference which I think highlights the charm and simplicity of type theory without delving in technical details too much. The syntax of set theory is in two layers: there are sets, and there are propositions (about elements of those sets). In contrast, there is only one such "layer" in (dependent) type theory: types.

Types play the role of both sets and propositions if you want to encode set theory in type theory. The point is that types can be much more than either of those things, and that idea is inherently difficult to convey to someone whose only conception of logic is sets and propositions.

Thanks for sharing this! These tidbits of history are fascinating.

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 details see Turner 1985, Thompson 1986. This feature was little used and has since been removed from the language. "

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.

Is that something he did to people who mis-cited his language?!

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, and then I went to look for a source for it and that grew into this whole blogpost.

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 construction like you describe to show that yet another problem ("symbol-printing") is undecidable, and that one is much more similar to halting than circle-freeness. Again, this subtlety is discussed in the paper.

I think you were a bit quick in dismissing the OP paper based only on its title.

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, Introduction to Metamathematics

They also bring up the "symbol-printing problem" present in Turing's 1936 paper, which is trivially equivalent to the halting problem with today's hindsight. That paper has a well nuanced take with a lot of interesting information.

For verified Rust there is also https://github.com/creusot-rs/creusot

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 better for different scenarios?

How does this compare to using simd (like simdutf8)?

This post is rendered at https://sugawarayuuta.github.io/charcoal/

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.

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 about what you want to say.

[1]: https://www.amazon.com/dp/0134080416?tag=duckduckgo-d-20&lin...

> 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 productivity of things like language choice.

How do you concretely do that? The initial paper, even if flawed, did a lot of work to try to control for confounding factors. To do what you said, you would have to put as much effort, if not more, to convince people that the results can be falsified to claim anything, with the same level of control in place.

It's not even clear that counting commits is entirely meaningless. Getting some signal out of it does seem tremendously difficult, but not impossible. So questioning the methodology is really the only way to rebut the experiment.

> 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.org/wiki/Defunctionalization

> defunctionalization refers to a compile-time transformation which eliminates higher-order functions, replacing them by a single first-order apply function.

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)).

> 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 orthogonal to the matter of automation/metaprogramming, which, from the lack of mention, doesn't seem to be their focus right now. There doesn't seem to be anything fundamentally in the way of Coq-style tactics either if they really wanted to build that on top of what is presented here.

> 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.fstar-lang.org/

I don't have any experience with "business" code, but my naive understanding is that application-level code is typically very monomorphic which is exactly where refinement types are useful, whereas the OP leverages polymorphism to a large extent (not necessarily), and that works well for general-purpose libraries which don't and must not care about their users' data.

> 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 unique, the number of possibilities is extremely limited. In the case of `Put` you can return either the new state or the old one. It takes a single unit test to ensure it's putting the new one, with parametricity to generalize from one case to all cases, still without looking at the implementation.

> In the second case, why do we have a program at all? If there is only one correct program we could have written then it seems to me that the program is in fact the type and the compiler ought to have been more clever and written it itself. (There are of course plenty of issues with that statement).

Program synthesis being basically proof search, even after the right automation is developed it may still be more practical to write the program by hand.

> They are particularly useful in proof assistants like Agda where one must manually exhibit a million trivial propositions and holes help fill in all the boring gaps.

I think the same mechanisms and benefits are at play here in a non-dependently-typed setting, even considering "entirely writing a function for you" as an unwarranted exaggeration.

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 the code can be generated automatically is an active area of research (program synthesis), but as this post already shows, for "simple" cases, we're getting pretty close.

As the post mentions, there are certain dead giveaways of an incorrect implementation, such as unused variables. Conversely one may still have some rough idea of the desired code to guide the implementation. The point is not about entirely removing one's mind from the process, but to allow oneself to only think about the choices that matter, which are few.

Alternatively, another way to look at the problem is that these types, while already being quite precise, are still not as precise as they could be, because the type system is not sufficiently expressive. And even with the ability to describe the desired properties to uniquely determine the implementation:

- it may not be obvious that the implementation is in fact uniquely determined;

- a solution, unique or not, may not be easy to find automatically. Program synthesis is essentially the same problem as proof search (c.f. Curry-Howard correspondence); knowing that there is a proof of Fermat's last theorem is not sufficient to construct an actual proof of it from scratch.

For these reasons, it may still be desirable to nail down the implementation explicitly even if it is hard to read.

It's also worth considering the fact that polysemy (the package that the controversial snippet at the beginning of the post comes from) is very much an implementation of a state-of-the-art effect system using state-of-the-art features of Haskell's type system, so it can be expected that the abstractions to make this code more digestible (for the right audience) are still missing, because no one has ever thought of how to express them yet.

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 implemented from scratch, and then you'll also want to write proofs about them.

- I had to reinvent IO in Coq.

- Most AOC problems are actually not that well-suited for formal verification. (It's certainly no fault of the AOC organizer!)

In particular, a lot of them basically ask you to simulate some system which doesn't have particularly interesting properties, so the implementation itself is often the best specification of the problem, and the main point of using a language like Coq is lost.

I did find some interesting problems though. For example, day 5 was a simple rewriting system and the question was to find the normal form of some starting string. Well, who's to say that the answer is unique? In this case it's easy enough to convince oneself that the given system actually is confluent, but I set out to prove it formally (and (re)learned a few things about rewriting systems on the way). (c.f., Confluent_react_steps, react_steps_injective, in day_05_common.v)

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 compiler that could be verified in principle. The CertiCoq project is actively going in that direction.

It does not.

aurman. More choices can be found here https://wiki.archlinux.org/index.php/AUR_helpers