Posted: Mar 20, 2012 10:00 pm
by mizvekov
epepke wrote:People who get really into LISP seem to become hostile to everyone else. So LISP didn't really stay with the times. It sort of lives in its own special world. It doesn't have to be this way at all; this is just what happened. I saw this in one of the posted (by @[color=#CC0000][b]VazSkep,[/b][/color] IIRC) links, arguing that LISP wouldn't help you with Perl, but you shouldn't be doing anything in Perl anyway. This, I think, represents a misunderstanding of what Perl is for and a failure to understand that writing beautiful programs isn't always the right thing to do.

It's funny you should say that, because at the time the guy who wrote it died, I remember reading a lot of people still partially blaming him for the failure of LISP to become popular, because he made their community seem much more hostile to newbies.

VazScep wrote:I'd expect you to be. I've thrown you in at the deep end wearing concrete shoes. :grin:

Hah, should have known it was a trap!

Right. Actually, I've used the axiom twice with two different instantiations. Rather than doing the instantiation manually, you might find this function helps:

Code: Select all
-- matchMP ( Γ ⊢ (P → Q) (Δ ⊢ P') attempts to match P with P', and then applies MP.
matchMP :: Theorem String -> Proof -> Proof
matchMP imp ant =
  let antT = concl ant in
    case theoremTerm imp of
      p :=>: q ->
        case match p antT of
          [insts] -> MP (UseTheorem $ instM Var insts imp) ant
          _       -> error "MATCH MP"
      _ -> error "MATCH MP"
This function is like mp, but it will try to instantiate the second argument to make it line up with the first.

Okay, thanks!

VazScep wrote:It might be that you are trying to prove something that is more aptly derived from the exercise theorem. Note though, that it took me 16 proof steps in all to do this.

Well ok, will keep that in mind :grin:

VazScep wrote:Yeah, there's a fair bit of work to go. My Bootstrap file is 425 lines of proof.

Hopefully that one proof is much smaller than that...

VazScep wrote:Not sure. I'd struggle to be able to give a definition of computer science and what a computer science degree should entail. At one end, if it's just the professional degree of a programmer, then I guess they should be expected to learn as many trade skills as a mechanical engineer :dunno:

I wouldn't be able to give that definition either. Computer science falls more within either formal disciplines or engineering than science itself.
But it's just that I feel that if your time in the university has done it's job right, then you should be able to pick up and learn anything new just by yourself. So I think that the teachers should focus more on the languages and tools which make their job showing new concepts easier, even if they are not widely used in the corporate world.

VazScep wrote:Heretic! If it types, it's correct!

Yeah, maybe there's more to this, or maybe less. I'm just trying to think of reasons why Common Lisp was made to be so dynamic.

:grin:
Sometimes there is no deeper reason than just "because they could and it was easy", and in fact I think that having no distinct types helps a lot here.

VazScep wrote:The sort of security I don't have is security from a malicious programmer, who perhaps used "Obj.magic" to circumvent the type system, or exploited a vulnerability in the Ocaml interpreter, or customised the pretty printer to render his trivial theorem that "1 + 1 = 2" as the statement of Fermat's Last Theorem.

Okay, I see :)

VazScep wrote:I can imagine a world where we actually start paying people large sums of money to do significant formalisation work. We'll probably have to be more concerned then with cheaters.
Don't get your hopes too high on that though :)