I think you should rather ask GP "How do you know that?". The link to the about page of Lean doesn't back up the claim that you can only write programs that halt.
And indeed, you can write programs that do not halt. You just have to explicitly tell Lean that you want to do that.
Yes, that is incorrect. If you write `partial def foo : Nat := foo + 1` it will be accepted, but `def foo : Nat := foo + 1` is not. So while lean checks that functions terminate by default, it is possible to define and run programs containing general recursion. This is subject to some restrictions though:
* You can't unfold the definition to try to prove `foo = foo + 1` (which is of course false for any natural number), it is an "opaque" definition and its value for specification purposes is essentially arbitrary and does not need to match the definition.
* Even then there is a possibility of proving false things as in `partial def loop : False := loop`, so to prevent inconsistency the target type (`Nat` in the previous example, `False` in this one) must be inhabited (proved automatically by the typeclass machinery). So it would reject the `loop` example but not `foo`.
The syntax is consistent, I don't know about the semantics. The trade-off is that it becomes more difficult to glance at a piece of code and visually distinguish what's what.
Datafrog doesn't use differential dataflow. Datafrog also requires you to do index management and joins manually, but it's very performant. Some of the join strategies are super optimized, but they don't allow for certain things that may be desirable, like negation/anti-join with a dynamic relation.
