Buffer overflow a crime? It's a fucking artform! Like stack redirection and overlaying. Damn. Kids today...

In reference to your post in emergence why is theorem-proving important?

SpeedOfSound wrote:Buffer overflow a crime? It's a fucking artform! Like stack redirection and overlaying. Damn. Kids today...

In reference to your post in emergence why is theorem-proving important?

One of things I am trying to say in that thread is that if importance is measured in numbers of bent-spoons, I'm failing to measure up. Programming wants to be engineering, but like religion and philosophy, it ends up being a popularity contest.

How do you feel about strong typing? If you're a fan, there's some seriously fucking cool stuff I can talk about, and it ties in beautifully with theorem proving. Otherwise, you'll find it kind of stupid.

VazScep wrote:

SpeedOfSound wrote:Buffer overflow a crime? It's a fucking artform! Like stack redirection and overlaying. Damn. Kids today...

In reference to your post in emergence why is theorem-proving important?

One of things I am trying to say in that thread is that if importance is measured in numbers of bent-spoons, I'm failing to measure up. Programming wants to be engineering, but like religion and philosophy, it ends up being a popularity contest.

How do you feel about strong typing? If you're a fan, there's some seriously fucking cool stuff I can talk about, and it ties in beautifully with theorem proving. Otherwise, you'll find it kind of stupid.

I am completely torn between two poles on strong typing. As long as you can over-ride everything the I am a fan. I came up with c and loved the ability to create my own little creature classes and do anything with them. I remember Pascal had frustrated me horribly. I used to call object programming 'granularity' before it cam to be a pop concept and I isolated my grains completely. Of course with c you only agreed to follow the rules, like gentlemen. I wanted to take the first compiler that insisted on following them and throw it against the wall!

I would like to dig into some of these new languages but not sure if I have the time. Tell me a about a pretty thing or two. I've got my head inside medium densely spiny neurons right now so I will probably disappoint you.

SpeedOfSound wrote:I am completely torn between two poles on strong typing. As long as you can over-ride everything the I am a fan.

You have no constraints when you're in front of a Turing machine.

"It's not about what the language makes possible; it's about what it makes easy."

When it comes to brass tacks, the difference is that typed languages make it easy to write typed programs and make it difficult to write untyped programs.

I would like to dig into some of these new languages but not sure if I have the time. Tell me a about a pretty thing or two. I've got my head inside medium densely spiny neurons right now so I will probably disappoint you.

Take implication in logic. I gave two axioms governing the logic of implication earlier on in the thread. Here's the first:

p → q → p

Now in Haskell, if you ask for the type of the constant function, you get this:

Code: Select all

> :t const
const :: a -> b -> a

As I suggested in the OP, there's more here than a mere analogy. Implications are the type of functions. If I tell you that p implies q, I'm telling you that I can meet the specification that inputs a p and outputs a q.

From there, the strength of the analogy goes crazy.

bookmarking