Viewing profile — pyrex41

Learning about Shen is what inspired the project for me. Combination of sequent calculus and prolog in a highly portable lightweight kernel that is easy to port to many runtimes ( …

Definitely connected; OPA is itself a structural gate, but at runtime. The post focused on compile-time gates, but there's no reason a structural gate can't run at runtime — which …

For a single-language Rust project with a handful of invariants, not much. Rust's newtypes + private fields + Result-returning constructors are exactly the right primitives, and th…

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 Turi…

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 …

I would add, re: Shen -- it's sequent calculus and unique type system (type system itself is Turing complete) give you a lot of flexibility here.

If you are the kind of person that immediately reaches for this solution -- then I agree, yes you should. You could even do it in Shen! ( https://news.ycombinator.com/item?id=39602…

I think you're right on the substance. A production-grade spec (or guard type) needs stronger assertions than the toy example in the post — predicates for signature verification, c…

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…

Author here. The TL;DR: move rules from prompts into types the compiler refuses to violate, then bounce the AI coding loop off those refusals. The repo is github.com/pyrex41/Shen-B…

And, given need to allow for errors in estimation and eventual deterioration of many alpha-generating strategies, adjusting investment fraction downward (a sort Bayesian prior, I s…

This is also an argument for finding investments that allow you to better define the downside risk of investments. I think that this is why static investments or hedges have such v…

Most of the examples of Kelly criterion application are either concrete bets with discrete payoff/loss odds and values, or assumed to be normally distributed. This paper discusses …

The reasoning behind the Kelly Criterion was explored recently in a more broad context, showing that the logarithmic utility is not required: https://aip.scitation.org/doi/10.1063/…