The problems of provable (formally-verifiable) program safety and determinism became crucial in the age of modern LLMs. I am developing #AluVM and @CationLang as a constructionist and ultrafinitist tool: in each type is a finite set of constructable objects; so there is type N8 made of all natural numbers (0 is not natural!) in range 1-256 included, N16, N32 and N64. There are integers of the same sort (0 included), I8, I16, I32 etc. There are no floating-point numbers, only rationals (in the Norman Wildberger @n_wildberger style), no sine/cosine - only rational trigonometry. Integers are pairs of numbers, not just “unsigned with a sign bit”, rationals are pairs of integers (i.e. quadriples of numbers). It uses dependent types (calculus of constructs), but restricts to finite types only. All functions are total, the termination analysis proves that. There is no recursion which can’t be reduced to a provable-terminating computation at compile-time. This gives a language and computational system which is formally analyzable at compile-time, by its structure.additionally to that, a binary compiled code is also formally analyzable and has a verifiable properties.

The failure of Rust language to ship with a proper concurrency is a language killer. I have fought it for 4 years with @cloudhead by applying reactor pattern in RGB, Cyphernet, @radicle - but now I am giving up. Rust is for the business logic, which must be separated from a scalable I/O (client or DB connectivity). For backends, this business logic has to be called via ZMQ-styled MQ from a runtime written in some other language with a proper native concurrency (Go or Elixir), not a retrofitted/backported one (like in Java, C#, Python etc). A niche for alternative language which fixes the gap between native concurrency and low-level system safe code is there. That is one of @CationLang goals, but it will take decade(s) to fulfill.

I have spent a lot of my time over the last two years designing a programming language which allows to (relatively easy) write a correct by construction code, i.e a code which formally verifies itself and does a lot of logic at compile time. The language is called cation @CationLang, which is a feneric programming language. Its dialect Contractum is made for smart contracts running @UVioletAI (RGB successor and superset). You may think of it as Lean 4, but able to do what you usually do with Zig. The new age of vulnerability discoveries highlights the importance of such language. Human programming is still at the amateur stage, and we need a new generation of tools to write software which is provably safe.