Leans proof checker is not polynomial time, unfortunately. It is super exponential. Basically, because it can verify the result of any function it can prove to be total.
740 karma · joined December 9, 2014
Of course I don’t know how it got its ideas for what to try. But heck, I don’t even understand how I get my ideas half the time. But the process, like what code it wrote, simulations it ran etc can be understood by (some) humans just fine!
I think it depends on your district. On some distros (looking at you arch!) I think GHCup and keeping things in /home and out of your system package manager is the better approach.
That said, I never had issues with Pandoc on any distribution. But I have struggled with Pandoc extensions, before I got NixOS (and flakes).
My experience and disillusionment is different from yours. I was inspired to do research from nerdy blog posts from researchers in my field. And my experience has mostly been that people in my field are honest, hard working, genuinely interested in doing their research as well as possible – mostly to satisfy their curiosity and sharing their findings with others. Any disillusion I have experienced has been about the fact that doing research is more or less something they squeeze in between teaching, applying for money and administrative tasks.
Even critical remarks are in the spirit of "You should do this better!", never the kind of gate-keeping bullshit I have seen in other fields.
It usually takes me two or three iterations to get there though. Discussing design and principles before writing the bulk of the code is a must. And then a pass or two of review to weed out ugliness.
Still saves time compared to writing the code by hand. Especially for tricky things, where type checking and tests can verify correctness.
For instance, in Sweden, to cherrypick a stat, in 1875 only 1% of military recruits were found unable to read [1].
We really must stop thinking that people of yestertimes where so much inferior to people today. Yes, there were differences between men and women, but this was also starting to change.
[1]: https://history.state.gov/historicaldocuments/frus1876/d308
But the 50% I do take into account, improves the text! And, like TFA, I never ask it for concrete text. It only helps me diagnose the issues, I prescribe the medicine!
False, at least from an American or Northern European perspective.
In the 1800s reading was an extremely popular activity. Not something restricted to a few. Printing press had been around for ages and the majority of the population read.
This situation suits me fine, since I am anyways more of an ideas person, than a crunching open problems person. But I understand the desperation of my colleagues who mad solving hard problems their identity.
I don’t know the details of RH, it might very well be solved soon, but it could also be impossible or just so difficult that even orders of magnitude more intelligent AI can’t solve it even.
If it is impossible to prove, it might be possible to prove that it is impossible to prove, or that itself might be difficult or impossible…
My branches end up in a tree structure (no shit!), and I rebase and merge up stream as changes land. I guess it could be more automated, but the only tedious part is remembering to remove old worktrees and prune the old branches
Part of the appeal of the Plan 9 approach was that you could use any program in your distributed environment, written in any language, because the abstraction layer was the file system – the lingua Franca of IO.
Oh, want to use that other machine as a gateway? Just mount its /net.
Oh, want to route audio through another machine? Just mount their soundcard into your /dev.
Oh, your machine is too puny to do the task at hand? Just run “cpu thebigmachine” which transplanted your entire environment over there (all the virtual file systems) so that you can continue doing what you were doing, but using that machine’s CPU and memory.
This solved the problem of having to transplant your setup to the remote machine, which you have with modern SSH. If you wanted a different environment you instead created it locally. Each process har its own virtual file tree with mounts.
There were cool things at the local level too: All the programs would expose virtual file systems to interact with. Text editor? Each window had a directory with files containing window content, current selection, even the UI “tagline” with commands. This meant you could write scripts for your programs in any language, because you just had to interact with files.
A modern take on plan 9 is definitely on my Christmas wishlist!
I have used Fable for formalisation and it will, unless I catch it, reprove results it previously had proven, inline, in other results.
My experience is that it takes a lot of human input to make Fable write code nice enough for a formalisation library others can work on. But since this is certainly a lot of prerequisites formalised as well, it would be nice if not all of the effort was wasted on one capstone proof! (Repost of a earlier comment, but I feel it fits better here)
My experience is that it takes a lot of human input to make Fable write code nice enough for a formalisation library others can work on. But since this is certainly a lot of prerequisites formalised as well, it would be nice if not all of the effort was wasted on one capstone proof!