Formal Verification Gates for AI Coding Loops

Re:Formal Verification Gates for AI Coding Loops by pyrex41 on Wednesday May 20, 2026 @04:06PM (#48213367)

Shen has some really unique properties that are under-developed here. It's type system itself is Turing complete and very flexible / expressive. Also, the Shen kernel is extremely compact, and easy to port into a wide variety of runtime languages (C, Lisp, Ruby, Python, JS, Go, etc https://shen-language.github.io/#downloads). What I discussed about using it as a compile-time gate + codegen is just scratching the surface, I think.

Now, a lot of the ports haven't been maintained. But the underlying Shen kernel is only 4-5k lines of code...remains extremely portable. More discussion here https://news.ycombinator.com/item?id=39602472

I didn't focus a ton on Shen in the blog post, because the underlying principles aren't really about the implementation. Shen is very cool tho.

[ Parent | on HN ]

Re:Formal Verification Gates for AI Coding Loops by zozbot234 on Wednesday May 20, 2026 @04:54PM (#48213993)

> It's type system itself is Turing complete

That's not a good thing! A Turing complete type system means that compilation is potentially undecidable and non-terminating. The whole unintuitive mess in dependently-typed systems about "definitional" equality (loosely speaking, a notion of equalities that are 'trivially' checked as part of evaluation) is entirely about avoiding Turing-complete type checking!

[ Parent | on HN ]

Re:Formal Verification Gates for AI Coding Loops by pyrex41 on Wednesday May 20, 2026 @05:04PM (#48214109)

I mean yes, that's a risk, and you are correct. In practice, is your spec about the shape of the app you want to build really going to be that complicated?

But I mentioned its Turing completeness as a lazy shorthand to illustrate that it is far more flexible and expressive than what people think of as a "type system". https://shenlanguage.org/OSM/Recursive.html

[ Parent | on HN ]