Comment by gobdovan
11 hours ago
Depends really. I tried some experiments towards a pretty uniform relational language for expressing ordinary logic, temporal logic, requirements etc. It does work, but there's some unexpected obstacles.
You'd think performance would be easy to achieve because you'd just write clear, high-level declarative facts and LLM + good optimiser + proof certification system will get you there in terms of performance. But you'll be surprised that relational/declarative specification gives you so much behaviour 'for free' that choosing what to actually compute from those relations is a very deliberate choice. It starts to look like finding an imperative-like path of demand through the relations. It seems that you get exactly the same problems but one level up.
I've enjoyed embedding declarative syntax inside imperative languages, like LINQ and prolog as a dsl. The imperative code can express temporality much easier, and the declarative code allows you to throw that away when you don't want it.
Coming at it from another angle, we have historically made distributed systems manageable / 'verifiable' with RTOSs which give deterministic scheduling and locking primitives. We know that a task's max duration is its uninterrupted duration + max duration of all higher priority tasks which could pre-empt it, and so on. Deterministic pre-emptive scheduling and locking alone could be enough to prove a lot of invariants without full temporal logic, and writing code in 'RTOS logic' might be more natural for humans/LLMs than the more expressive and powerful alternatives.