sordina

Curry Howard shows that for a logical proposition (A) with corresponding constructive proof (B), there will be a type (A') with program (B'). It's not about proving desired properties of programs. However, you can use the CH principles to do this too, as long as you can encode the proposition about a program in its type. This will not often look like the dataflow type of the naive program though. Look at software foundations for real detail, I'm not expert at this stuff, just aware of the basics.

Mate, the point I was making is that 15 minutes is not a reasonable time frame to learn new programming concepts in.

You've got the right idea. A program is a proof for the proposition made by its type. Only for the right languages though, and not in the naive sense of `assert(1+1 == 2)` proves the assertion.

Well, I interpret that as the assertion that it's more opaque than other types of programming. But I disagree and think that it is actually simpler in terms of the syntax and amount of prior understanding required. My blunt reply is that to assert that a particular example is inaccessible but then only to have dedicated 15 minutes to prove so is silly. I'm sure most people who seem to suggest that this stuff is opaque had no problem learning PCRE or complicated SQL joins and also didn't complain that it took more than 15 minutes to do so. Of course TT is a deep field and there are many complicated parts of it, but the syntax, rules and the example given are not opaque and very understandable to anyone who can tackle languages and abstraction.

What part am I ignoring?

If someone can learn C type syntax this is MUCH simpler. That doesn't mean you don't have to spend a little bit of time learning how it works, but it is not some kind of number-theory level maths construction only accessible to savants.

15 minutes is not a long time. Easily understand doesn't mean instantly understand with no background reading.

Pithy but useless sentiment.

So if you implemented it with analog circuits that would satisfy your criteria?

So if you lost the weights how is that not killing the AI? Is it because it lacks the death experience? If so what about bitrotting the weights incrementally and degrading its inputs?

The HTTP examples are fine, but a lower-level network module would enable all sorts of amazing plugins like a JDBC style ecosystem (WDBC?).

> generates more than 20 million dollars a year of revenue

and

> team is 3 people

and

> post COVID, budget is really tight

Why? All technical details aside if this can't be addressed I wouldn't even bother trying unless I owned stock.