It seems some kind of arbitrary execution is necessary. I decided to come back to the problem out of curiosity to see if I could push that toward declarative or logic to gain its benefits. This isn't another argument so to speak so much as a brainstorm pushing envelope here. Could speculate all day but came up with a cheat: it would be true if anyone had replaced make or other imperative/arbitrary pieces with Prolog/HOL equivalents. Vast majority of effort outside I/O calls & runtime itself would be declarative. Found these:
Add to that Myreen et al's work extracting provers, machine code and hardware from HOL specs + FLINT team doing formal verification of OS-stuff (incl interrupts & I/O) + seL4/Verisoft doing kernels/OS's to find declarative, logic part could go from Nix-style tool down to logic-style make down to reactive kernel, drivers, machine code, and CPU itself. Only thing doing arbitrary execution, as opposed to arbitrary specs/logic, in such a model is what runs first tool extracting the CPU handed off to fab (ignoring non-digital components or PCB). Everything else done in logic with checks done automatically, configs/actions/code generated deterministically from declarative input, and final values extracted to checked data/code/transistors.
Hows that? Am I getting closer to replacing arbitrary make's? ;)
...I'm not sure I totally understand. Here's how I'd solve the problem:
Each filetype is accepted by a program. That program is what we'll want to use to compile or otherwise munge that file. So, in a file somewhere in the build, we put:
*.c:$CC %f %a:-Wall
*.o:$CC %f %a:-Wall
And so on. The first field is a glob to match on filetype,%f is filename, %a is args, and the third field is default args, added to every call.
Target all is run if no target is specified. The first field is the target name. The second field is list of files/targets of the same type, to be provided to compiler on run. It is assumed the target and its resultant file have the same name. The last field is a list of additional args to pass to the compiler.
This is something I came up with on the spot, there are certainly holes in it, but something like that could declaritivise the build process. However, this doesn't cover things like cleaning the build environment. Although this could be achieved by removing the resultant files of all targets, which could be determined automatically...
There you go! Nice thought experiment. Looks straight-forward. Also, individual pieces far as parsing could be auto-generated.
Far as what I was doing, I was just showing they'd done logical, correct-by-construction, generated code for everything in the stack up to OS plus someone had a Prolog make. That meant about the whole thing could be done declaratively and/or c-by-c with result extracted with basically no handwritten or arbitrary code. That's the theory based on worked examples. A clean, integration obviously doesn't exist. The Prolog make looked relatively easy, though. Mercury language make it even easier/safer.
http://www.cs.vu.nl//~kielmann/papers/THD-SP-1991-04.pdf
https://github.com/cmungall/plmake
Add to that Myreen et al's work extracting provers, machine code and hardware from HOL specs + FLINT team doing formal verification of OS-stuff (incl interrupts & I/O) + seL4/Verisoft doing kernels/OS's to find declarative, logic part could go from Nix-style tool down to logic-style make down to reactive kernel, drivers, machine code, and CPU itself. Only thing doing arbitrary execution, as opposed to arbitrary specs/logic, in such a model is what runs first tool extracting the CPU handed off to fab (ignoring non-digital components or PCB). Everything else done in logic with checks done automatically, configs/actions/code generated deterministically from declarative input, and final values extracted to checked data/code/transistors.
Hows that? Am I getting closer to replacing arbitrary make's? ;)