Additional time axes allow you to separate transactions from different sources of input. E.g. in a collaborative system it could be helpful to ask questions while rewinding the actions of a particular user.
But a different question is whether the system can do something useful for you with first-class time co-ordinates, compared to just stuffing additional timestamps into your data. (something useful being clever indexing, compaction, maybe more?)
If model-theoretic semantics and the various ways to slice, dice, and extend Datalog are interesting to you, then almost any talk by Peter Alvaro might be as well.
I think Finda (https://keminglabs.com/finda/) fills a similar need, runs offline, and indexes lots of other stuff as well. Although I think it is not possible to assign additional keywords.
Jonathan Blow's language "jai" allows for seamlessly switching between AoS and SoA and generally seems to value efficient data layout and "gradual" optimization over safety (in contrast to e.g. Rust).
Unfortunately, no public compiler seems to be available at this time.
For anyone interested in exploring the datomic model, there is a great ClojureScript in-memory implementation called datascript (https://github.com/tonsky/datascript) by Nikita Prokopov.
We use Datalog every day in a React-Native application, via the datascript db (https://github.com/tonsky/datascript).
Has been a very positive experience so far.
Thinking in "facts" / binary relations is itself a refreshing approach.
That was not the intension behind my comment at all. I rely on type systems a lot, myself.
I was trying to note that Clojure, as a dynamic language, is making a (to my eyes) very interesting choice, of doubling down on these dynamic methods of verification. For some uses, I can see this as the better choice, for others it isn't and won't be.
As a side note in his talk "Simple Made Easy" (https://www.infoq.com/presentations/Simple-Made-Easy, around minute 42)
Rich Hickey mentions, that conditional statements are complex, because they spread (business-)logic throughout the program.
As a simpler (in the Hickey-sense) alternative, he lists
rule systems and logic programming. For example, keeping parts of the business logic ("What do we consider an 'active' user?", "When do we notify a user?", etc...) as datalog expressions, maybe even storing them in a database, specifies them all in a single place. This helps to ensure consistency throughout the program. One could even give access to these specifications to a client, who can then customise the application directly in logic, instead of chasing throughout the whole code base.
Basically everyone involved agrees on a common language of predicates explicitly, instead of informally in database queries, UI, application code, etc...
But Hickey also notes that this thinking is pretty "cutting-edge" and probably not yet terribly practical.
Full, formal verification of complex systems (especially in the distributed case) requires a lot of modelling effort, beyond what is needed for "mere" implementation. A lot of important constraints cannot even be expressed in most type systems. And if one uses a specialised modelling language for the proof, the actual implementation might introduce bugs.
Also relevant to real, shipping software: specifying a program in such that detail as required for automatic verification makes it even harder to change (which, given infinite time and money, is indeed a very very good property!).
This just goes to say, that a type system can be very helpful, but is ultimately just a part of regular testing.
So for most companies and most developers, anything that aides in keeping documentation up-to-date, writing or generating tests and helping developers understand what they are reading is probably a better ROI.
You make a very good point, the comparison was flawed there.
> The thing I do see as being important is not how you write these things down, but whether they have an accessible representation at run/read/compile/whenever time.
This is a better way to put it. The second important factor for me is expressiveness. With spec or any other contracts-like system one gets the full power of the language to express constraints. Of course type systems are not artificially restricted in this regard, they simply make a different trade-off.
I hope my comment did not come off as a riff on static vs dynamic typing, and I don't think any contract system is meant to replace type systems. Until expressing all important program specifications formally becomes viable for everyone (maybe through this work https://www.math.ias.edu/vladimir/current_work?), a less-formal, dynamic approach seems very attractive.
Clojure, with its dabbling in schemas and rule systems / logic programming (as a substitute for conditional statements) and thanks to its great tools (like figwheel or devcards), could really be establishing a cheaper, "as-good" alternative to static typing and full formal verification.
Instead of encoding constraints as type signatures, the Clojure folks (true to character) encode them in data. In my eyes a very interesting, pragmatic trade-off between expressiveness and automatic verifiability.
BlitzBasic and BlitzMax are about the same language. What BlitzMax provided over BlitzBasic was a direct integration with DirectX and OpenGL, which allowed you to make 2D games with hardware supported rendering.
Your average BlitzBasic "Hello World" would usually take up 50% of the CPU.
I spent most of my early programming years with BlitzMax.
The language itself probably has no future on it's own, but combined with the DX/OpenGL integration and overall straightforwardness, I'd heavily recommend it for interested children.
But a different question is whether the system can do something useful for you with first-class time co-ordinates, compared to just stuffing additional timestamps into your data. (something useful being clever indexing, compaction, maybe more?)