upvote

points

by pyrex419 hours ago |
comments
upvoteby elfly2 hours ago|
next
[-]
This is great but keep in mind that Go allows the programmer skip these invariants in various ways.

I wish Go had a serious type system. Never mind algebraic types, but one that fucking respected private values and did things like validating enum values.

reply
upvoteby ajb5 hours ago|
prev|
next
[-]
TBH something like this sounds useful even without LLMs (although I haven't fully grokked this yet). The problem with the operational level is that you can't express the invariants etc at the type level - not least because you're working across multiple languages - so the kind of dumb issues that we're beginning to rule out at the level of the language at the process level still require lots of diligence in operational code. Some kind of shared "operational type system" that could be integrated into relevant languages would potentially help a lot.
reply
upvoteby pyrex414 hours ago|
parent|
[-]
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.

reply
upvoteby zozbot2343 hours ago|
parent|
[-]
> 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!

reply
upvoteby pyrex413 hours ago|
parent|
[-]
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

reply
upvoteby Mikhail_K7 hours ago|
prev|
next
[-]
Thank you, interesting work. Please, clarify what is possibly a naive question - your README states that the constraints imposed by your tool are weaker than the formal verification guarantees. Why not implement the backpressure as the full formal verification barrier? Too complex to implement?
reply
upvoteby pyrex416 hours ago|
parent|
[-]
The distinction worth keeping clean is between the spec (here, written as proofs in Shen) being formally rigorous and the entire codebase being formally verified. Shen-Backpressure does the first: the spec is a sequent-calculus statement of invariants, and shengen lowers it into guard types the target compiler refuses to violate, so within the target language's type discipline you cannot construct a tenant-access (or any other witness) without discharging its premises.

It does not do the second (formally verify the entire codebase). Outside the guard types your Go or TypeScript is just code. It can panic, race, have bugs in unrelated logic, use reflection to forge values inside the guard package, get a wrong answer from the SQL query that fed the predicate, and so on. The proof ends at the projection boundary.

Why not go further? Not really "too complex to implement," in theory; it has been done before. But verifying the whole program is much higher engineering cost, and the trades-offs to do it make sense in a much narrower set of cases than what I'm trying to target: teams shipping production code with AI in the loop, in the language they already ship.

The pragmatic choice is to spend the verification budget on the small set of invariants that genuinely matter and leave the rest as ordinary code with ordinary review and tests. That is why the claim is phrased as "practically impossible to accidentally bypass, not categorically impossible to bypass." Over-claiming "verified" when the host language is unverified would be misleading.

reply
upvoteby alasano7 hours ago|
prev|
[-]
[dead]
reply