Notices by Philip Trettner (artificialmind@fosstodon.org)

@lisyarus nice! Do you have a good reference for the virtual pipes model? I did shallow water equations using the discrete exterior calculus in my masters thesis but was disappointed by the "flow feeling"

@aras imagine the panic in some manager's head:

* avg systems programmer does like 25 LOC per day (according to some study-thing)
* they could have got a daily rate of like 2500 moneys for you
* you produced -50000 LOC

.. excel quick maths ..

you cost blender about 5 million moneys!

(do we need /s here on masto?)

@lritter @sinbad @TomF Have you played/seen Astroneer? One of the best diegetic interfaces I've seen in a survival crafter.

(You are actually carrying your inventory on your back. You always see what's in there and it's also where you interact with it.)

@julesh There is still a gap as far as I understand it: there exist functions that are computable and total but where the totatily cannot be proven inside the same system. This should be a consequence of Gödel's incompleteness.

However, the CIC can represent almost all of math, so I don't know if such functions can exist in practice. How do you "know" that it is total while being unable to prove it?

Like, I think you can prove their existence but never provide an example. (I'm fuzzy on this)

@julesh I think that's basically what the Calculus of Inductive Constructions (as used in Coq / Lean) provides.

The syntax only allows recursion on structurally smaller arguments.

Recursion on inductive types is always well-founded and you can define inductive types for a well-foundedness relation, which basically means that all provably total functions are definable.

The syntax ranges from "reasonable" (any obviously structural recursion requires no annotiation) to "custom proof required".