AI Assisted Proofs

Compared to model checkers that just exhaustively search a well-defined state space, there's not a lot of reason to believe in opaque, large proofs of interactive theorem provers at this moment. Four reasons. 

1. There's a problem with the math. If there's one 'paradox' like Banach-Tarski, there are probably an infinite number of them. What if the proof exploits one?
2. There's a problem with the logic. At one point in time, I understood the rather simple type theories people worked with. I don't understand the current ones, so maybe I shouldn't comment on it, but I am unsure how robust they are. 
3. There's a problem with the implementation of the type theory. Usually, that would boil down to a kernel bug, but there's ample reason to believe it may lie elsewhere. For example, the presentation of a proof.
4. There's a problem with the formalisation. I.e., something was stated, but it turns out that didn't reflect the math correctly, and subsequently something else was proven.

I don't really trust these latest proofs, but at the same time, I am not that sceptical. I would call it a coin flip.

Peirce's Law in Egel

 Like Scheme, Egel has a trivial inhabitant of Peirce's Law ((p->q)->p)->p too.

def peirce = [F -> try F [X -> throw X] catch [X -> X]]

The combinator peirce has Peirce's law as type and takes as an argument a function F of type (p->q)->p and we feed that function another function of type p->q that throws its argument X of type p to the outer scope.

Utter bullshit, of course. 

Matching recurring variables

The Egel interpreter is about a decade old, and I thought I kinda milked it already for all the blog posts I wanted to write about it. 

 The best overall feelings I have about the interpreter can be summed up as: A) It's a fine toy esoteric language, but please don't use it professionally. And B), I have a lot of fun coding Advent of Code solutions in it, and there's something to the language, but I cannot quite pinpoint what. 

Someone asked me where Egel would fall compared to other languages, and I am not entirely sure about that either. Q/Pure, Maude, Wolfram Language or something defined in Racket might be close. 

Refal came up during that discussion, and I looked into it. One thing that struck me is that Refal can pattern-match recurring variables. I could extend Egel with that, maybe. That would allow definitions like `def eq = \x x -> true | _ _ -> false`. It seems non-trivial, but on the other hand, all the machinery should be in place. But at the same time, it doesn't seem to useful a feature.