|
|
|
|
|
|
by jcora
2632 days ago
|
|
|
This can be done, for example ST in Idris which lets you reason about resources (check out linear types). However, if you are thinking more in the direction of "you have to reason about where and how exactly your values and functions are stored", you're moving back to C, because the entire point is to disentangle the formal description of computation, from it's actual execution in the real world. If you want to deal with that, you have to do it explicitly and _by reasoning about it_ (with ST, for example). Which is what purity means. > They are "total" only with respect to a set of axioms which imply an execution model where computers do not explode mid-program "There is a chance that the computer blows up" is one of those things that have little bearing when reasoning about programs, it's just not in the domain of discourse. It certainly has no formal bearing on the notion of totality, mathematics just doesn't deal with cases such as "what if everyone who counted to 5 suddenly died", it deals with the counting itself. When the chance is actually high, for example radiation in space flipping bits, I'm pretty sure you want to handle that elsewhere. It's not hard to imagine a fault-tolerance system gaining a lot from dependent types, however, with their ability to prove that your code follows a defined protocol. |
|
|
(One of my favorite topics, that I've written about in other threads!)
https://news.ycombinator.com/item?id=15560845
Check out how the city seamlessly regrows after you nuke it:
https://www.youtube.com/watch?v=XkSXERxucPc
> Robust-first Computing: Distributed City Generation: A rough video demo of Trent R. Small's procedural city generation dynamics in the Movable Feast Machine simulator. See http://nm8.us/q for more information.
And here's a robust, self-healing membrane, that tolerates random failures (like tiny little exploding computers):
https://www.youtube.com/watch?v=oq0uvF4mm7Y
>To demonstrate the robustness of three membrane implementations in the MFM, an instance of each was placed side by side and subjected to a failure probability of 5e-5 per site per EPS. That is, each site is erased, on average, every 20,000 event cycles.
Intercellular Transport also demonstrates some robust chemical and biological programming metaphors:
https://www.youtube.com/watch?v=6YucCpYCWpY
>Two cells are interconnected by self-healing wire. The magenta substance is being passed from the cell in the west to the cell in the east. The black particles are an ectoplasm, allowing the membrane to identify sites outside of the cell. Similarly, the yellow and blue particles are an endoplasm specific to the cell in which they reside, allowing the membrane to identify sites inside of it.
Demon Horde Sort exemplifies the Robust First approach:
https://www.youtube.com/watch?v=helScS3coAE
Into functional programming? Here's a demo of programming the Movable Feast Machine with λ-Codons:
https://www.youtube.com/watch?v=DauJ51CTIq8
>λ-Codons provide a mechanism for describing arbitrary computations in the Movable Feast Machine (MFM). A collection of λ-Codon molecules describe the computation by a series of primitive functions. Evaluator particles carry along a stack of memory (which initially contains the input to the program) and visit the λ-Codons, which they interpret as functions and apply to their stacks. When the program completes, they transmute into output particles and carry the answer to the output terminals (left).