The new bane of my existence, uncommented Coq code.
ef_deterministic ef = true ->
forall ge args m t1 t2 vres1 vres2 m1 m2,
Events.external_call ef ge args m t1 vres1 m1 ->
Events.external_call ef ge args m t2 vres2 m2 ->
(vres1,t1,m1) = (vres2,t2,m2).
Gee thanks... Not only is one of the most conceptually complex languages mankind has come up with, it has that single letter fetishism that mathematicians tend to have.
Ah found the full video
This testing technique would probably be good to compare how *nix lego programs are working between operating systems.
Really miss GOFAI and lisp in AI. Guess it is time to open that topology book, before the engineers make planet killing AI from their lack of understanding of measure spaces.
Thanks. I hate it.
Controlling for mental limitations seems to be a common theme in the formal sciences such as math and software engineering.
"In this paper, we have tended to stress simplicity above all else because that is the first filter for any proof."
Good mathematicians are suckless devs.
Excuse the naiveté, but what is the deal with languages and operating systems that organize themselves around one feature? From an SE perspective, that seems like a lot of work to adapt your own compiler, or kernel and package system, over a single selling point.
Rust, memory safty
Haskell, lazy evaluation
Guix, hashed/functional package management
InstantOS, fast wm
I am a logician that likes computers
A mastodon instance created by Derek Taylor, creator of the DistroTube channels on YouTube and LBRY. Derek is an advocate for free and open source software.