discarded1023

Enjoy it mate, and all the other fat Brunners. (His Stand on Zanzibar is most of Gibson's Neuromancer ... more than a decade before.) Give the thin ones a miss.

On a related note, for those who don't mind reading 17k words on industrial decline, is Ian Jack's great take on (civilian) shipbuilding in Glasgow.

The relevance to TFA is the difficulty of recovering the arts of ship construction lost to offshoring, financial engineering, politics, whatever. And it's a great read.

[1] https://www.lrb.co.uk/the-paper/v44/n18/ian-jack/chasing-ste...

I wonder how this relates to the old combinator-based approaches of Peter Henderson [1] and the logic-programming version [2]. Guy Cousineau also had a go with "Functional programming and geometry" in the late 1990s. I guess we'd say these are capable of describing corecursive pictures now.

I always felt this stuff would make a better foundation for web layouts than CSS.

[1] https://dl.acm.org/doi/pdf/10.1145/800068.802148

[2] Logic programming, graphics and infinite terms P. R. Eggert, K. P. Chow Department of Computer Science University of California, Santa Barbara UCSB DoCS TR 83-02 June 1983.

The author, Larry Paulson, may or may not like ZF but he has a ton of experience in doing formal proofs in it.

https://isabelle.in.tum.de/website-Isabelle2020/dist/library...

The standard arithmetic classes of Isabelle/HOL show that you can extend division with the equation `x / 0 = 0` and things (seemingly) work out.

https://lawrencecpaulson.github.io/2021/12/01/Undefined.html

https://www.hillelwayne.com/post/divide-by-zero/

https://xenaproject.wordpress.com/2020/07/05/division-by-zer...

You'll need to do some thinking/proof to find out if it works for you.

A cognate of this is what Gernot Heiser of seL4 fame calls the "McNamara Effect" on his homepage: https://gernot-heiser.org/

> The first step is to measure whatever can be easily measured. This is ok as far as it goes.

> The second step is to disregard that which can't be easily measured or to give it an arbitrary quantitative value. This is artificial and misleading.

> The third step is to presume that what can't be measured easily really isn't important. This is blindness.

> The fourth step is to say that what can't be measured really doesn't exist. This is suicide.

> I want a good notation for state machines that is similar to EBNF.

If this isn't a firm requirement, perhaps you can dig into the venerable state machine notations of yesteryear. For instance ARGOS [1] and StateCharts [2]. The latter got incorporated into UML somehow [3] IIRC. Esterel [4] is a bit mind blowing.

Other people prefer dataflow, in which case Lustre [5] might be worth a look.

These make a strong synchrony hypothesis which may or may not apply to your situation. But if it does you're in clover. And if you're not you can still try to use this stuff in a GALS [6] architecture.

[1] https://dl.acm.org/doi/10.1016/S0096-0551%2801%2900016-9 (and google some more) [2] https://statecharts.dev/ [3] https://en.wikipedia.org/wiki/UML_state_machine [4] https://en.wikipedia.org/wiki/Esterel [5] https://en.wikipedia.org/wiki/Lustre_(programming_language) [6] https://en.wikipedia.org/wiki/Globally_asynchronous_locally_...

I don't disagree with what you say here, but ... I'm coming at it from a formal semantics point of view. (I find Prolog and indeed "logic programming" in a larger sense to be all promise and little delivery on this front.) Perhaps you can check if your `prove` example is expressible in HiLog ... if so, it's more-or-less first order (in a semantically clean way). I believe the hard working XSB have an implementation.

Higher order functions! -- in Prolog! oh my.

Prolog has predicates, not functions. (It has uninterpreted function symbols -- aka functors in this context.) It's based on first-order logic, i.e., it has nothing higher order in it, if you want to take it (formally) seriously. But of course there is `call/1` and so forth, which are just hacks... err, "non declarative".

There are some interesting higher-order logic programming languages, e.g. Mercury. I like the approach taken by HiLog [1] as it struck me as (semantically) honest and simple. I don't know if it's usable.

[1] https://en.wikipedia.org/wiki/HiLog

I don't disagree with your stance but one of the most beautiful things to come from this line of work was Ehud Shapiro's declarative debugging [1]. I'd recommend taking a look at his PhD thesis if you're at all interested in what logic programming can do (that nothing else can [2]). You can also see it as a philosophical exercise: he shows how we might understand Popper's falsification criterion and use it to do science.

[1] Tech report: https://cpsc.yale.edu/sites/default/files/files/tr237.pdf

[2] There have been attempts to build declarative debuggers for other languages but for one reason or another (complexity, space use, incomplete coverage of the language, ...) they don't appear to get used very widely. Shapiro's setup is beautifully simple for what it does.

Here "declarative" means that you have a model in mind ("model" in the sense of logic, i.e., you expect your predicates to hold of particular arguments) and the tool helps you explore the divergence between what you wrote and what you intended. Thinking this way means you can completely ignore the details of SLD-NF resolution (the details of the Prolog implementation)... I mean, it's unlikely to be perfect in practice for any number of reasons, but I find it very disappointing that we don't dream like this any more.

I learnt as an undergrad that every sufficiently large program contains a type system (in the loose PL sense of operations requiring arguments of certain sorts) ... now that can be provided by the language or in an ad hoc way by the program itself. (Yes, shades of the CLOS truism.) Python has learnt this lesson (at least I get this impression from reading hacker news) since I stopped using it circa 2015.

As for modes, well! 1. they were needed for at least one Uni of Melbourne person to receive their PhD degree, and less facetiously 2. they are needed for efficient code generation. They can be inferred for this purpose. One use case you may consider is enforcing the correct dataflow in a DCG. Otherwise they are handy for preventing calls to predicates that would not terminate.

I've never programmed in Mercury but it really looks like an ML to me. It was beautifully engineered in the late 1990s and it's a shame it hasn't received more attention. Its FFI influenced the development of Haskell's.

There was a lot of work done in the 1980s and 1990s on deductive databases. Somehow it didn't work out. See [1] for a survey from 1995 (coauthored by the most cited guy in CS). There is also the semantic web with its query technology. Also didn't work out.

[1] https://www.sciencedirect.com/science/article/pii/0743106694...

What do you mean by "misappropriated"?

You can try running with what wikipedia says [1] or stack overflow [2]. You could say it's PL marketing terminology from the 1980s and 1990s (FP + Prolog v the world). Roughly these languages aren't based on the idea of changing state, but of course that idea eventually ends up in there somewhere (e.g. monads and laziness in Haskell, DCGs in Prolog).

On the positive side, I'd be comfortable saying that SQL is declarative.

I'd be wary about bringing Turing completeness in here. It seems irrelevant.

[1] https://en.wikipedia.org/wiki/Declarative_programming

[2] https://stackoverflow.com/questions/129628/what-is-declarati...

There appears to be a lot of activity around minikanren [1]. Personally I'm so used to having a powerful metalanguage around (lambda calculus plus or minus a bit) that I can't imagine programming in pure Prolog any more. Which is to say this is probably the way to go in practice, if a subproblem can be solved using logic programming.

[1] http://minikanren.org/

> Prolog also requires you to understand the execution model before you can do much of anything.

This is true of most (all?) languages. Prolog's control flow is ultimately not too different from the usual stack-based semantics people are used to from imperative languages like C (if you're not too ambitious with the backtracking; if you are, best of luck!). The tricky part is perhaps understanding the dataflow that arises from unification. That can be arbitrarily complex but it seems people tend to go no further than difference structures, which are easy to comprehend in terms of pointers. (Yes yes I know, but logic variables are essentially just single-assignment pointers.)

The thing I find deeply weird about the logic programming literature is that if you want to reason about your program you're told to use things like Hoare logic [1] or intended interpretations [2] and not fundamental logical concepts like implementations implying specifications (ala Lamport and many others who grappled with refinement).

[1] see Krzysztof Apt's papers

[2] see e.g. https://people.eng.unimelb.edu.au/lee/papers/dd.html

Prolog has many issues; for instance the lack of types and mode declarations, and backtracking almost never being what you want. This was addressed in Mercury [1] but much of the baby was thrown out with the bathwater. (IMHO Mercury ultimately landed closer to the MLs than to Prolog.) The academic literature suggests classic Prolog got fast enough in the late 1980s / early 1990s on stock hardware [2]; see also Peter Van Roy's intriguing book [3] for what happened next.

IMHO it's worth learning about Prolog as a way of looking at the world -- for instance Isabelle and Lambda Prolog are essentially logic programming engines, albeit with more sophisticated terms and unification algorithms.

[1] https://mercurylang.org/

[2] https://www.hpl.hp.com/techreports/Compaq-DEC/PRL-RR-36.pdf

[3] https://www.info.ucl.ac.be/~pvr/book.html

Indeed! Gall's SYSTEMANTICS [1] is worth a read in its entirety.

[1] https://en.wikipedia.org/wiki/Systemantics

Try Standard ML or ocaml. You may be surprised how far the module system can take you, and how limited type classes really are for expressing abstractions. On a different vector, you can see the same story -- type classes are convenient but too limited -- in the development of abstract algebra/topology/analysis/... in Isabelle/HOL.

As for laziness, things don't work out too well for a variety of reasons. Bob Harper laid out several many years ago. See e.g. https://news.ycombinator.com/from?site=existentialtype.wordp...

So many memories! But how many of you are a god of twenty-first century computer science? https://www.geocities.ws/robrich18/Larry.html

Like the strict MLs (ocaml, Standard ML, F#, ...), while Lisp and Scheme can express the Haskell idioms it lacks the pervasive laziness that makes them (somewhat) efficient. For instance one might write `zip [0..] xs` to number the list `xs` in a single pass. This lack of laziness (even on code that does notionally work without it) manifests in blowing stacks, in Scala at least. Also the lack of types (type classes) precludes at least some things such as the `deriving` mechanism.

For all that you're dead right about Python.

"Red Plenty" by Francis Spufford. Many pointers from Google:

https://www.google.com/search?q=red+plenty

It's a fictionalised history of some Soviet economics. There's a chapter on Kantorovich (cf the sibling comment). It goes reasonably deep (not mathematically deep) and provides a lot of context. Great book from a great author. Don't be put off by the "Soviet" part -- it's very entertaining.

Not to dispute your points in any substantial way but the fundamental R&D for China's solar panel industry was substantially funded by the Australian tax payer. See, for instance

https://www.abc.net.au/news/science/2021-09-19/solar-panels-...

Also I think Delhi's air pollution is the worst of the major cities now.