burakemir

I heard SHACL helps with specifying structure (shape), and more so than OWL which is more about meaning (and where it may be acceptable to have an incomplete but "open" specification).

Programming with these structures (triple/quad with shape constraints) would be interesting, general-purpose programs could not easily take advantage in the form of static type-checking. This is roughly the same type of problem as the "object-relational impedance mismatch." I believe some kind of type-checking (shape-checking?) for SPARQL queries might be possible, but don't know if any such thing is implemented.

RDF comes with this whole set of W3C standards, and standardization seems to be a big point in favor if you need to care about interoperability.

In terms of data model, RDF may be a bit too web centric to be approachable. Linked Data does not seem much better.

This may not be a fully informed view, but so far I think: While the whole area of (broadly) logic-based representations (including datalog, eg. Souffle, datomic, ...) seems to have a bit of a renaissance, all the semantic web stuff seems a bit more like baggage.

In other words: if I wanted to build a private knowledge base, I don't want to pick or publish URIs and the fact that all the documentation pushes me towards open/sharing is just getting in the way.

In contrast to that, relational databases tech has affected programming languages and frameworks over the decades and goes way beyond triple/quads (e.g. LINQ, or relational mappings). This seems to be a big missed change in a way since, some of the "typing" would in principle be a lot closer to class-based OOP then all the relational stuff.

The stack is real and reminded me of Data-Context-Interaction https://dci.github.io/. Its inventor Trygve Reenskaug was arguing that this helps with building UIs and object models that are closer to how users think about the world (which should be related to product design.)

Thank you so much for taking the time to reply.

I now realized that I confused "syntactic" and "semantic" completeness.

I agree on your points; my first up there was ignoring a bit of the context (it was late...) and not meant to "motivate" the multitude of proof assistants by incompleteness theorem.

As a programming language person, I am quite convinced there will never, ever be an agreement on a common formal language (even if there was or is agreement on foundations it should be based upon) - it is the same as for programming languages.

This is more due to human nature rather than technical factors, and if we conceive logic as a linguistic activity, then we can see how foundations and the corresponding ergonomic language logic are related, maybe two sides of the same coin. "Foundations" in the context of mathematics appear (to me at least) as something technical and interchangeable.

Is there a venue for discussions on logics like these outside of the occasional logic-related HN threads? : )

Let me try to reconstruct what has been said. You seem to be reacting to points different from the one I tried to make.

bjornsing: All of mathematics can in principle be derived from ZFC. morelisp: not all, there are independent statements. Mathematics is beyond formalization. bjornsing: like what? are you saying that formalization is futile? or not? me: CH is an example. formalizing is not futile, but affected by incompleteness theorems in the sense that all those proof assistants, when used for developing some theory, will require something else to prove the consistency of that theory.

dwohnitmok: the point of incompleteness is not that it requires a stronger system, but that a weaker system cannot prove a stronger system, killing the idea of trusted computing base.

See, I was not trying to expound the significance of the Second Incompleteness Theorem; I do not really care what mathematicians consider as in or out of "all mathematics," but I noticed that "being able to formalize all mathematics" has become a somewhat technical expression in logic.

I like very much what you're writing in that comment. I have also seen Gentzen's consistency argument for PA and think the qualification that you include at the end about weaker systems sometimes being able to show the consistency of stronger ones is needed.

I did not imply that proving consistency of X within X is desirable.

However, I am intrigued by Artemov using a provability operator to prove consistency of PA in PA: https://arxiv.org/abs/1902.07404 Provability logic is interesting, a modal logic that adds Loeb's theorem as axiom (maybe Carl Hewitt would consider it a foundation of computer science? but I digress.)

Now, the reason I feel compelled to comment back: I do not understand why you bring up completeness. What are you reacting to? Are you trying to imply that using incomplete foundations is the key to ignore the challenge of proving consistency?

Saying "ZFC is enough for all mathematics" is a commitment to ZFC axioms and to first-order logic. First order logic is compact and complete. As such, it is very much affected by the First Incompleteness Theorem and also the Second, and there will also be non-standard models and the Skolem paradox.

I don't have a horse in the foundation and formalization race, just curious what you mean. As far as I can tell (and I may well be off, not a mathematician), it seems quite desirable that foundations worthy of the name would let us prove all theorems of arithmetic and natural numbers.

The continuum hypothesis is an example of a statement that is independent of ZFC.

About futility of theorem proving: I think a useful perspective on this is that the context of formal logic with respect to "all mathematics" used to really mean "all of mathematics in one system" a hundred years ago.

This is the logicist program started by Frege and Russell - make everything formal - and this was shattered.

Now nothing stops us from formalizing some part of mathematics. Today, when people say "you can formalize all mathematics" post Gödel, it means you pick your area and formalize away, knowing that effectively proving consistency of your formal system (within the same system) is out of reach.

So nobody tries to claim "all in one system" but many logics and sets of axioms coexist without there being any distinguished one that is better (in the sense of effectively proved consistent and strong enough to be "useful").

"Let's see how this essential complexity claim holds for a couple of things I did recently at work:"

"For some queries, it's arguably zero — my work was necessary only because of some arbitrary quirk and there would be no work to do without the quirk. But even in cases where some kind of query seems necessary, I think it's unbelievable that essential complexity could have been more than 1% of the complexity I had to deal with."

It's very clear that the author of the post understands "essential complexity" as related to thinking about the query they need to write (data structures).

The issue is that in today's computing environments application programming is only a fraction of solving the problem of delivering the application.

They too see the essential (or inherent) complexity as being a domain and requirements related thing, but they draw the conclusion that they are somehow not part of it.

It is possible the whole app and system would be unnecessary if the essential complexity was addressed differently.

And it is also possible that due to the current way of doing things, there are new sources of essential (inherent) complexity.

Brooks couldn't have foreseen productivity gains coming from the internet and collaboration. But if you factor all that in and create a new baseline, faster machines still don't tell you what is the best way to deal with changes in requirements or how to represent a postal address so that it works internationally.

Typo: Hindley and Seldin ... silly phone autocorrect

The article is a deep dive into Moses Schönfinkel's life, and mentions how his work is picked up by Haskell Curry.

It is very long, contains surprisingly few of the characteristic Wolfram promotion usually found in Wolfram texts, but besides a detailed biography and pictures of historic documents, there are a few gems (people who researched "algebra of logic" before most others) for the persistent reader.

> And maybe if the operation we now call currying needs a symbol we should be using the “sha” character Ш from the beginning of Schönfinkel’s name to remind us of a person about whom we know so little, but who planted a seed that gave us so much.

That's a good suggestion!

For folks who are interested in combinators but didn't get what they want from the text: the approachable reference on combinators is Hindley and Sheldon's "Lambda-Calculus and Combinators: an introduction"

... and of course, there is "To mock a mockingbird" by Raymond Smullyan, which introduces the topic through puzzles.

(Googler here) The article is a good description of the tools, and I was not aware of the blaze clones plz and pants.

One thing that is maybe not obvious: For an API author, code search in combination with a monorepo and the somewhat hermetic universe which is Google's code base provides immediate access to all uses of a library. You can see what worked well and what didn't, and it enables effective refactorings. That also means when writing a client, you can quickly figure out from other client code how stuff is supposed to be used. All this makes code search such an effective tool in Google's development environment (in the broader sense).

If anything like this were possible for open source (indexing code that depends on a library/API, across subrepos in any version control system, in a way that gets near complete coverage), it would enable similar possibilities of systematic improvement.

Alas, it does not seem realistic except in a few niches where the number of clients is bounded and code owners are willing and able to follow a protocol (approve changes to their code that unblock such global improvements.)

Nah: the article says the CAP narrative is based on very specific assumptions which make it unfit to talk about actual distributed systems.

Gödel's incompleteness (that, by a diagonalization argument, formal systems of minimal expressivity will contain true statements that cannot be proven) applies and will continue to apply to all such formal systems. The bar is so low that any interesting formal system is affected by it. Also, it does not make math broken at all - those formal systems can and in fact must be consistent for the proof to go through (1st incompleteness theorem), and it's just a pity that whatever formal system one comes up with, if it contains arithmetic, it won't be able to prove it's own consistency (2nd incompleteness theorem).

In the words of von Neumann: Gödel's two past papers ("Widerspruchfreiheit" and Continuum Hypothesis), are in any case worth more than the total literary output, past, present and future, of most mathematicians [...]

This got me thinking about how "module" - a language concept - is about bringing in definitions (values, types...) into scope, but then there is deployment, something being "installed at a version".

Modules, understood as such, are inevitably connected to the stuff that is happening "one level above" where these things providing the modules are installed (Rust crates, npm packages).

Reaching for a language-independent word, I'd propose to call these things "components" (slightly longer-form thoughts here: https://blog.burakemir.ch/2020/07/modules-components-and-the...)

... but those things happen to be called (or heavily associated with) "module" in Java, C++20 and go.

This piece is intended as an accessible intro; it talks about the beginnings of formal logic, how intuitionism in the debate on foundations of mathematics led to intuitionistic logic, and Gentzen's natural deduction.

It seems the only other HN discussion about a post on natural deduction so far was this one: https://news.ycombinator.com/item?id=22324836

There is also one on Curry Howard: https://news.ycombinator.com/item?id=17748717

It's from there that I found "Howard on Curry Howard", a published response to a letter Phil Wadler wrote to William A. Howard. It provides an excellent hint how Martin-Löf's work on dependent types was influenced by the Curry-Howard correspondence and natural deduction. https://wadler.blogspot.com/2014/08/howard-on-curry-howard.h...

This looks like a nice project, and I will check on its progress. So far only two of the advertised steps are there.

Reminds me, I started a RISC emulator project on a holiday - and then forgot about it when the holiday was over :o

Not sure if combining "learn rust" and "learn RISC V" at the same time is a good combination for a large audience, it will depend on the reader.

Maybe the intended audience is someone who knows enough basics and has plenty of motivation for/prior knowledge of/interest in both topics. And then, for good content, there will always be an audience.

Covid-19 ist the disease. https://www.who.int/emergencies/diseases/novel-coronavirus-2...

The virus itself is called SARS-CoV-2 and previously 2019-nCoV

https://en.m.wikipedia.org/wiki/Severe_acute_respiratory_syn...

In Switzerland, health insurance may be private, but is mandatory and there is a large catalog that even the cheapest insurance must cover.

On the other hand, the state (each canton) pours large amounts of money into hospitals and research. There are laws and regulations at various levels (edit: eg how many doctors may open a new cabinet), and in these days we are reminded that doctors can be mandated to work when a crisis requires it.

Calling this a "completely private healthcare system" is a bit misleading.

Your statement is wrong, in the following sense: at runtime, the call to x.foo() would always start look at the runtime type (which in this case is Bar, or some subclass of it) - otherwise overriding methods would not work.

https://docs.oracle.com/javase/specs/jls/se7/html/jls-15.htm...

TL;DR Swiss firm Crypto AG sold tech to governments for decades, but turns out to be owned and operated by CIA and BND who benefited from backdoors. From their POV, a wildly successful operation, beyond imagination.

> At times, including in the 1980s, Crypto accounted for roughly 40 percent of the diplomatic cables and other transmissions by foreign governments that cryptanalysts at the NSA decoded and mined for intelligence, according to the documents.

This looks quite interesting, thanks for sharing.

I found the other recent thread on technical writing useful, too: Four kinds of documentation https://news.ycombinator.com/item?id=21289832

Sabine Hossenfelder discusses science and scientific method. She points out that falsifiability is an inadequate criterion, Occam's razor and that climate change deniers are quite unmoved by evidence since they are unable to tell what science is.

There is something in here that is relevant to models, of any kind.

> The more and the better data you have, the higher the demands on your theory. Sometimes this means you actually need a new theory. Sometimes you have to adjust one or the other parameter. Sometimes you find an actual mistake and have to correct it. But more often than not it just means you neglected something that better measurements are sensitive to and you must add details to your theory. And this is perfectly fine as long as adding details results in a model that explains the data better than before, and does so not just because you now have more parameters. Again, there are statistical measures to quantify in which cases adding parameters actually makes a better fit to data.

The post is a speculation whether a January 1957 paper, "Programming the Logic Theory Machine", by Newell and Shaw might be the first published use (or "definition") of the term "programming language".

It is always interesting to look at beginnings and early signs of notions - concepts - that we use in our everyday lives. The particular phrasing, I don't know if that should matter so much.

Chomsky's work on formal languages falls roughly in that epoch of 50s, ALGOL and COBOL, too.

"Computing" wasn't what it is today, I think mathematical and electrical engineering background of the computing experts would affect what language (pun intended) they used. The idea (and term) of "languages" stayed but what makes a term popular is hard to settle.

I think in terms of concept, formal (mathematical) logic predates all this by a few decades. The subtitle of Frege's 1879 "Begriffsschrift" was "Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens" which I would render as "A formula language of pure thought, modeled after the arithmetical one". I think the roots are rather there...

Thanks for this comment and the anthology. Indeed the whole question is a bit odd and one ought not to glorify calculi but study them.

Lambda calculus originated from research in formal logic, which is about manipulating symbols according to precise rules that would capture reasoning. It is a compelling way to combine variable binding, equality and substitution into a model of "function calls" - even if the purpose was to formalize arithmetic computation and reasoning.

At some level, reasoning is what programming is about as well! The notation and rules may change, but ultimately we want to make the machines do things and at some level, we need abstraction mechanisms. Recursive procedures are such a mechanism and it can be expressed as a lambda term that involves a fixed-point combinator, or machine code.

It is easy to model and understand many things using lambda calculus or functional programming techniques, depending on whether the interest is theoretical/formal or practical.

To quote Peter Landin (heavily influenced by McCarthy and LISP and author of 'The next 700 programming languages'):

> A possible first step in the research program is 1700 doctoral theses called "A Correspondence between x and Church's λ-notation."

Maybe people think this was different in the late 1950s?

Let's read McCarthy's paper 'Recursive Functions of Symbolic Expressions and their computation by machine Part I' where he explicitly cites Church and introduces lambda notation.

I would consider that paper part of the phenomenon that is LISP, would that not settle the question? Lambda calculus gives little guidance in terms of implementation, but I think it does not diminish LISP in any way that it should be "based" on lambda calculus.

And I do not find the linked article adds any value, but I am very glad to read the HN discussion to find gems like the above (even if I should rather have slept for the past few hours).

Nice post. Still, I find the most accessible article describing datalog is "What you Always Wanted to Know About Datalog (And Never Dared to Ask)." by Ceri, Gottlob, Tanca (1989)

I also found Awodey's category theory more helpful than Milewski's ramblings (though I appreciate his effort). Maybe it's because I find "applications in theory" worth learning.

If I may try to point out what's missing: it is the motivation which seems to get lost for lack of examples.

Here's a theory, called category theory, and many of us believe it can inform their designs, providing a perspective on compositionality, and a higher kind of equational/algebraic reasoning.

Where are the ideas and examples that will actually help us inform or designs and achieve a higher degree of compositionality? Where is our chance to apply algebraic reasoning to the programs we write?

  So I will provide a lot of C++ examples. Granted, you’ll
  have to overcome some ugly syntax, the patterns might not
  stand out from the background of verbosity, and you might
  be forced to do some copy and paste in lieu of higher
  abstraction, but that’s just the lot of a C++ programmer.

Maybe this would work, but we don't actually see it in Bartosz's posts. As a different example, take Wadler's papers on comprehensions and monads (rendered as Kleisli categories): the motivation is very clear, we'd like to express certain programs/queries within a functional programming language, and all examples contribute to an understanding.

What should an experience programmer learn? One suitable answer seems to be the connection of lambda calculus with products and CCCs. That, though, would also need motivation for "functional programming", referential transparency. An alternative answer could be to point out the connection between topos theory and logic (or query languages).

It almost seems that when flipping to Haskell examples, Bartosz is making a leap that let's him ignore the motivation: anybody who is writing code in Haskell won't need to be convinced of referential transparency. There is simply a forest of "patterns" and category theory seems to be a systematic path through it. Maybe potential applications in physics provide a similar motivation for physicists.

... but if you don't bring the motivation yourself, you're not going to get it from reading the posts.

You have to ask yourself whether, in the process of building that complex UI, you haven't invented another framework.

After the first few web apps, one necessarily sees the repetitive elements and wants to capture that in libraries and abstractions. Routing URLs? Reuse that widget? This is just coding instinct.

I think it is possible to have a stream of projects where each new one gets its framework copied and pasted from the previous. That does not mean it's not a framework, just one without name and documentation.

Then there are projects of a certain size that you wouldn't want to do like this. Stakes too high, more than 1-2 developers. Then you can either brush up your framework and give it a name and documentation and contribute to the 'problem' of too many frameworks.

Or use something that others use and is just as suitable.

The author is developing a theory of expressions (generalizations of list comprehensions) operating on 'ringads', which are monads with a few additional operations and laws.

The academic style probably blurs the fact that this has very deep practical applications, as it provides a framework that permits to write down database joins and OLAP multidimensional queries (including aggregation) in multiple ways that can be considered equivalent through application of monad and ringad laws. This in turn can enable us to interpret such expressions efficiently, by picking the one that corresponds to a desirable execution plan.

Another paper that I would consider related is the one that points out how comprehension expressions can express SQL features like 'order by' and 'group by', namely 'Comprehensive comprehensions' by Wadler and Peyton-Jones.