Working on finally releasing the programming language I’ve been working on for quite a while.

I’m setting up the basic site, which is not a huge deal, but I’ve been inspired by more recent language designers having a streaming presence, so I am working through test runs of streaming my development.

I hope to start with demos of the basic language features and then move on to streaming both a reimplementation of my compiler and on a Rocq implementation of the syntax and semantics of the language for proof work.

The language has a rather small niche at first glance, so I’m hoping to use the streaming as a way to explore areas of appeal and maybe draw some interest. A low level concurrent and parallel ‘functional’ language with very non-traditional syntax and a modal, dependent type theory is not going to appeal to everyone, but hopefully I can find some interest eventually, even if just to hang out on chat and talk about the subject.

▲

jesse__ 7 hours ago | parent | next [-]

> A low level concurrent and parallel ‘functional’ language

I'm not particularly familiar with array based languages, but are you inspired by them at all? Seems like a similar concept.

What're your goals for the language? It would be cool to see a parallel execution model unify SIMD, multithreading and gpu. I bet people with a lot of money would be interested if you could apply it to ML

▲

j-o-m 7 hours ago | parent [-]

Not particularly inspired by the array languages in general. I do like the idea of a specifics DSL or library that is built from the ground up for ‘vector’ operations (Futhark would certainly be an inspiration here). I do think an (syntax divergences aside) implementation of what is essentially CUDA-like language/library is very possible.

I don’t really have any lofty goals, the language exists to let me have my personal ideal programming language. One of the things I would like to see adopted, by any language, is that the language is able to encode and present provable guarantees about code. So, memory safety, freedom from UB, lack of overflow (integer or stack) is provable in some subset of the language and the proof is done in a logically consistent, verifiable manner.

Of course most of those proofs are not anywhere near feasible for general case code, but the language can restrict allowable constructs in a computation, function, process, or module to a set that makes the desired properties provable by construction.

The language should be capable of unifying and abstracting over SIMD (or other hardware implementations), GPUs, and OS or Userspace multithreading at levels of abstraction from assembly to Haskell or other high level languages.

	▲	jesse__ 6 hours ago \| parent [-]
		Cool, thanks for the response and good luck with your project!

▲

nodra 7 hours ago | parent | prev [-]

I look forward to seeing it.