pyrex41

7 ms·

1.
by pyrex41 4mo ago
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 ( https://shen-language.github.io ) gives a ton of e
2.
by pyrex41 4mo ago
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 means they compose rather than compete. I didn&#x2
3.
by pyrex41 4mo ago
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 they're strictly stronger than Go's (no reflect
4.
by pyrex41 4mo ago
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
5.
by pyrex41 4mo ago
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 r
6.
by pyrex41 4mo ago
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.
7.
by pyrex41 4mo ago
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=39602472 , https://news.ycombinator.com
8.
by pyrex41 4mo ago
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, claim-binding, and expiry-from-token, at minimum. The ex
9.
by pyrex41 4mo ago
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
10.
by pyrex41 4mo ago
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-Backpressure. Builds a lot on Geoff Huntley's
11.
Formal Verification Gates for AI Coding Loops(reubenbrooks.dev)
144 points by pyrex41 4mo ago|34 comments
12.
Real Decision Making vs. Expectation Value(aip.scitation.org)
3 points by pyrex41 8y ago|0 comments
13.
by pyrex41 8y ago
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 suppose) is sensible on its own, sans vol sensitivity conside
14.
by pyrex41 8y ago
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 value; they may not change the expected value, they might eve
15.
by pyrex41 8y ago
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 how extremely skewed outcomes (eg, stock options) shoul
16.
by pyrex41 8y ago
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/1.4940236 Taleb has a good discus