Conversation

@natecull I would... question that to one degree or another. There's a deep truth to the formal equivalency of computation models, and at a certain point, you're constructing your semantics based on the the semantics of the language you're writing in, which in turn is based on the invocation of the von Neumann machine and its merry copulations with the Harvard machine as time went on. So in a very deep way, if you can write it and it executes, it's derived from the Great Abstract Universal Computer and is a valid expression in that existence (it's 1:30 a.m. and my ability to communicate meta-abstractly without going a bit maudlin is slightly knappered).

that said, I grasp what you're saying. I would, however, suggest that until you define your problem to the rigor you desire, the thing is a bit smoke and mirrors. What exactly do you need that C, Ocaml, Prolog, Java, doesn't cover, given a certain amount of coding at the library level?

Do you need FOL, SOL, regexp, dependent types, all of that can be coded up within all of the above, if you're willing to suffer through the divers long and winding invocations of same.