jz391

You mentioned good tools available for Z - do you have any recommendations? I have tried in the past using VDM (alternative to Z, similar level) for writing down specifications precisely, but could never find adequate tools for maintaining/checking proofs/derivations.

In the UK, there used to be significant tax advantages in forming a Ltd: you could pay significant part of the income as dividends (since you were both employee/director and shareholder), which attracted lower tax & could be split with your wife etc. Then regulation IR35 came along...

This is a very interesting discussion. Your analogy of nuclear power is insightful to me. New technology with great positive & negative impact potential, some difficulty in controlling and a military applications (possible weapons-grade material production), being developed for commercial use.

Nuclear power development took different paths in different countries, with different government/private mix and light/heavier regulation (eg in US, AEC was supposed to both promote development _and_ regulate).

The central problem here is pace of AI development. It takes time to establish functional controls/laws/practices. I'm sure that in 1950s/60s, the pace of nuclear _military_ proliferation seemed running out of control. This lead to fear of falling behind (hence arms race), fear of nuclear war (CND) and some eventual stabilisation of the international landscape. However, the commercial development was largely unopposed, due to the techno-utopism of the era. Obviously governments found it much easier to control the public narrative at that time. Our societies are having this lively public debate now, before we have a good understanding (based on experience i.e. accidents/mistakes).

Another difference is that nuclear power involved only governments and v. large corporates, i.e. much fewer entities compared to AI use rollout to basically everybody in developed countries. Imagine the difficulties we would have faced with that technology, if consumers in 1960s had available nuclear-generated power which required them to exercise precautions to avoid radiation.

It is much easier to accelerate development of tech vs pace of societal processes such as public debate, law, regulations, broad understanding (aka "common sense"). I expect some artificial slowing down will need to be applied to the technology side, to allow the humans to catch up.

And, of course, with the Speccy you had the Microdrive - an affordable middle ground between tape recorder and a disk drive. I still remember the excitement of not having to record/rewind/play (to verify). Good old times...

That is sad to hear. I had the pleasure of meeting him once, working with Perihelion as a student. Perihelion were a smart bunch and Helios (quasi UNIX distributed OS for Transputers) was incredibly usable and powerful for its time and hardware (Transputers lacked MMU).

Would an extension to `madvise` to say: "page this region in/out as a whole" help here? Engine could define memory ranges representing each expert and leave paging to the OS (tho' "paging" at this point becomes more similar to swapping in granularity...).

One point mentioned in the first link you included is support of $ORIGIN in #! scripts - that would need kernel support.

I think many of us miss that feeling... For me, the level of complexity of the computers in my childhood (TRS-80, Spectrum) made them interesting but still possible to fully understand. I think we have lost that - modern hardware and software has complexity on a scale which makes it impossible to fully follow. After decades of computing, I only have a high-level understanding of many components of a typical PC. So for my son, any understanding of what's going will be difficult...

I do understand it takes effort to stop and re-accelerate, but isn't making effort (exercise) part of the purpose of cycling in the first place? My main objection is to cyclist failing to stop at pedestrian crossing lights: as a pedestrian, when I see a green light, I expect to cross without having to dodge moving vehicles on the road. I do check the the road to make sure that cars have stopped, but cyclists (who rarely stop at crossings, at least in London) are harder to see, as they are smaller and often obscured by the traffic.

Definitely agree with the sentiment (also a Speccy 48K guy), but at the risk of being pedantic, I think you're double-counting: "million times faster" is for one Spectrum, the "0.000625% price" is for a million...

Braces are substitution, so

  b{a/x}

means: expression b with variable x inside it replaced by expression a. So their beta-reduction line just says that if

  k = ... (λx.b) a ...

it can be reduced to

  k = ... c ...

where c is the expression b, but with all occurrences of variable x replaced by expression a.

I think Tk(x) denotes "the definition of variable k is expression x" and the square brackets are "k[x]" something like "in the context of definition k, value of expression x". So I suspect that

  a=Tk(x)
  a[y]

would be effectively

  (λk.y)x

But yes, not very clear on explaining the notation. Also seems to have some typos e.g. at the beginning have "x ∈ k, x, y" which looks to me should be "x ∋ k, x, y" (or of course "k, x, y ∈ x").

> I wouldn't call it "exceptionally nice"

I guess depends on your reference point :-) I recall in the beginning, python offering an easier/more readable alternative to Perl, which itself was a step up from awk/sed/sh script (for the tasks/uses GP mentions)

Reminds me of a commercial project I did for my old University department around 1994. The GUI was ambitious and written in Motif, which was a little buggy and leaked memory. So... I ended up catching any SEGVs, saving state, and restarting the process, with a short message in a popup telling the user to wait. Obviously not guaranteed, but surprisingly it mostly worked. With benefit of experience & hindsight, I should have just (considerably) simplified it: I had user-configurable dialogs creating widgets on the fly etc, none of which was really required.

The key issue is that Lisp's minimal uniform syntax has less variation to help with visual pattern matching, which we humans are good at (compared to richer syntax).

The meta-programming power of Lisp may be largely due to being homoiconic, although Dylan/Julia etc achieve similar without it. However Lisp's minimal syntax is not a prerequisite for homoiconicity: S-Plus/R has a more conventional syntax while retaining "code is a list" representation.

To extend your analogy: if the house is a listed building (UK concept; apparently US equivalent is listed in National Register of Historic Places), by law you cannot just tear it down. You need to do much more work to renovate what can be done without disturbing the original structure. This obviously costs much more and is generally done by different specialists, who have harder job and hence are better paid. So the question comes back to: what kind of work do you want to do...

And, of course, the next level of procrastination is to develop your own programming language, which you will use to write the engine to use in creating the game :-) Definitely hats off to Jon for pulling it off - he had a lot of focus and some previous experience - and it also helps to have re$ource$ from past successful games. For many of us, the lure of developing better tools, rather than the end product, proves to be too strong to resist. At least Jon stopped short of developing own OS :-)

True for many, but I actually have been acquiring some computing books I had enjoyed reading in my youth (e.g. Organick's Multics). Perhaps living permanently abroad strengthens nostalgia...

Interesting. The voice used for the pronunciation sound seems to be using the wrong language though (FYI using Firefox).

Absolutely. As an Electrical Engineer turned software guy, Ohm's/Kirchhoff's laws remain as valid and significant as when I was taught them 35 years ago. For software however, growth of hardware architectures/constraints made it possible to add much more functionality. My first UNIX experience was on PDP-11/44, where every process (and kernel) had access to an impressive maximum of 128K of RAM (if you figured out the flag to split address and data segments). This meant everything was simple and easy to follow: the UNIX permission model (user/group/other+suid/sgid) fit it well. ACLs/capabilities etc were reserved for VMS/Multics, with manuals spanning shelves.

Given hardware available to an average modern Linux box, it is hardly surprising that these bells and whistles were added - someone will find them useful in some scenarios and additional resource is negligible. It does however make understanding the whole beast much, much harder...

Indeed. Coming from UNIX tools (sed/awk/sh/grep/tr etc), perl had a lot of appeal and almost intuitive syntax - alternatives in the '80s being C, awk, or if you were unlucky, FORTRAN IV without string type :-). The benefit of having a single language with all of the functionality of these tools was amazing at the time and ability to use familiar syntax was a benefit. However expectations for programming languages grew somewhat since...

Does anyone have experience using any of these for scientific paper PDFs, in particular containing equations (I'm guessing graphs are still well beyond their reach)? The workflow for these seems to involve converting PDF->text...

Could be worse of course: Multics (the first system with hierarchical names) used greater-than (>) as separator. Unix/DOS use of slashes gives us the sane pipeline/redirection syntax we all love (see [1] for the Multics redirection syntax).

[1] https://retrocomputing.stackexchange.com/questions/7030/why-...

I understand what you mean (although I "grew up" on UNIX, don't find this a problem); however, it would be better if the long (i.e. readable) options were prefixed by double dash to follow usual UNIX convention.

Using single dash for single character options allows you to combine them, which is really useful (if you do remember these options of course), so `-exc` means `-e -x -c` etc.

Excellent Sci-Fi yarn, with nostalgic references. I particularly liked the VAX-11 and LISP reference ("ideograms in a formal language full of parentheses")

Not my area, but isn't a lot of NVIDIA's edge over AMD precisely software? NVIDIA seem to employ a lot of software dev (for a hardware company) & made CUDA into the de facto standard for much ML work. Do you know if AMD are closing that gap?

I've used Slickgrid (open source, https://slickgrid.net/) with some success.

Does anyone know if Cahit's Spiral Chains proof (<https://arxiv.org/abs/math/0408247>) was found to have issues? It is much more elegant, as it avoids the exhaustive computer case verification...

I believe the parent was referring to line from the article which said "...square that gets partitioned into rectangles of equal area" - i.e. area of yellow, green, pink and orange is the same, so the area of the big rectangle containing all those four colours must be 4 times the height of orange rectangle (since their widths are the same).

So another Banks' novel - "Look to Windward" - title came from this poem

Slightly odd that they explicitly say:

  these should include the lang attribute to identify the language

but then don't do that in the Example (with *vini, vidi, vici*)...