This isn't really a comment about dependent types, but one of the things I hate about environment variables is that you can't query a binary to ask what environ

This isn't really a comment about dependent types, but one of the things I hate about environment variables is that you can't query a binary to ask what environment variables it supports. Sometimes I wish I lived in the alternate universe where every executable binary on my computer had a machine-readable interface description that included every command line argument, every environment variable, every file it needs access to (if not provided as a command line argument), and all file I/O was strongly typed. Example use case of the latter is that if I have a postscript file and want to convert it to a pdf but don't know the name of the program that does it, I could run a solver that figures out that in a pipeline like this: "cat foo.ps | $converter > foo.pdf", ps2pdf could be substituted for $converter and result in a well-typed command line. This could be integrated into tab completion.