GDR

Things old games have taught you

Author: Sirocco
Subject: Things old games have taught you
Posted: Sat Sep 04, 2010 12:08 pm (GMT -8)
Topic Replies: 0

Looking back at some old games I enjoyed playing, I have to admit they have taught me some harsh lessons. There will be spoilers galore in this post, and likely a dash of profanity, but I'm going to detail moments in gaming that drove me batshit insane, to the point where I never want to make those mistakes in my own games.

1. Unannounced limitations are evil in long games - King's Quest 2 & 4

I have a love/hate relationship with all the King's Quest games I've ever played. I love them because they can be charming, technically astounding for their time, and full of crazy shit, but it's hard to love a game series that punches you in the junk at almost every given opportunity. The worst of these moments come when the game gives you an odd limitation, and either deliberately or accidentally fails to tell you about it. Two cases in point: the bridge in KQ2, and the shovel in KQ4. The bridge in KQ2 is particularly nasty, as it lets you cross it seven times before collapsing, and you need to cross it no less than seven times to finish the game. So, if you wander over the bridge even once to "see if anything has changed", you're hosed... and you won't realize it until you're at the end of the game and unable to cross the bridge that one last time. In KQ4, there is a shovel that is only good for five uses, and you need to dig up exactly five graves to finish the game. After five uses the shovel will break. You see where this is going, right? Also, how about that golden bridle? You know, the one that is hidden on an island that you can never return to? Yeah, you remember that, don't you, you sadistic whore! There's a special place in hell reserved for Roberta Williams, and I'll be there... merrily flaying the skin from her bones for all eternity. I may even do it with a golden bridle, just to make my point clear.

2. If there's an item I require to finish the game, don't let me lose or waste it - Ultima Underworld 1 & 2, Obitus

Ultima Underworld was an astounding game for its time. No doubt. It was also a mofo because it couldn't be completed unless you gathered a bunch of special items and used them to perform a ceremony at the end of the game. But... and I'm sure you know where this is going... it's entirely possible to lose the items permanently. For example, not knowing that I needed a particular book, I was doing some inventory management at the bottom of the dungeon and accidentally tossed it into a lava-filled chasm. I thought it had landed on the ledge next to me, but it skipped off into the nether regions of the game. Books don't float on lava, you know. I thought things were kosher, and went about my business, until I got to the end and realized I was hosed to the max. Fuck me.

Lightning struck twice with Ultima Underworld 2, where you need to have a flask of basilisk oil to complete a ceremony required to complete the game. There's only two flasks in the whole damn game, and the game doesn't note what the flask is good for until you need it, so it's easy to drink in the heat of battle and forget about. I figured it would have some sort of defensive effect, and also figured I could get some more. Like I said, there's one other flask, and it's a huge pain in the ass to find, even when someone tells you where it is. If you somehow lose both, you're hosed. Totally hosed. Fortunately, this time I located the second flask and went about the business of finishing the game, but in the back of my mind I always told myself the game's designers had attempted to assrape me, and missed by a just little bit, brutally poking my taint instead. Not a good feeling, man.

In Obitus, there are bosses that can only be killed by using special and purposefully rare magic powders of varying strength. Use the wrong powder on the wrong boss and you'll never finish the game.

3. Timed events in adventure games is a staggeringly bad idea - Rise of the Dragon, Dark Seed

So I need to buy some flowers to progress in the game, but the flower girl is only around for one day, then never seen again in the game. Also, I might need a stick, that I get while visiting my neighbor at 5 P.M. on one specific day, where he's playing fetch with his dog. If I miss that, I'm forever hosed. After all, it's not like I can just walk by any tree and get a branch off it, right? RIGHT? If you think either of these scenarios is appropriate, and think the approach would make for a fun game, please give me your address so I can stop by and fuck you with a rake before you can ruin the lives of so many people.

4. Arbitrary death is not a fun thing - Pretty much any game Sierra ever made, now that I think about it

Space Quest and Police Quest were probably the kings of arbitrary death (perhaps giving an honorable mention to The Immortal), taking sadistic delight in ending your game for making the slightest wrong move, or hosing you because you did something like hop in your squad car without doing the 360 degree safety inspection (I'm not joking, either). I've always felt that death in games should be something you can see coming, even if it's inevitable. There's something immensely saddening about realizing that you've just saved the game right after doing something that will result in a game over with 100% certainty, and haven't had the foresight or OCD to make multiple saves. Police Quest taught me that lesson: save often, and rotate your save slots, because the guy who designed the game you're playing just might be a motherfucker. Monkey Island 1 make fun of Sierra by having a sequence late in the game where Guybrush can accidentally fall off a cliff. This pops up a Sierra-inspired "You've died! Restart. Reload. Quit!" prompt for just a moment, before seeing the hero fly back up onto the ledge. He makes a joke about landing on a rubber tree, but we all know the joke was on Sierra for being such unrepentant dickweeds.

5. Sometimes less is more - Final Fantasy VI

I was replaying FF6 for, oh I dunno, the umpteenth time, when I was struck by how nonabrasive the game's dialogue was. It was a little cheesy at times, but the game never drifted into "full emo" mode like it did during 7, 8, 9, 10, and sometimes 12. Space limitations worked their magic, and while the game is stuffed to the brim with places to go and things to see, it doesn't have the space to wander through immense emo or metaphysical diatribes that plague many jRPGs. There is one, and only one, moment if self indulgence on the part of the creators, where the entire cast of player characters go all sappy and explain why their lives have meaning. It's still short compared to even a single conversation in modern games, and to top it off the final boss chides them for sounding like chapters from a self-help booklet, before launching an all-out attack. Many times I play RPGs to explore, and kick ass. Overly indulgent, droning exposition isn't something I relish.

6. Those other guys were good, but I'm the best bad guy I'll ever face - Ultima IV

In Ultima IV you are the only bad guy. Yes, you. You'll be in a full-on battle against your evil, self-serving proclivities, and the game will be throwing a gauntlet at you that requires you to abstain from all the stuff you normally do in RPGs. No stealing, no cheating, no overkill, no cowardly behavior, no backstabbing, no self aggrandizing, and absolutely, positively, NO MURDER. The sick point is that the game makes it easy to do all these things, often to the point of actually encouraging the behaviors it holds against you. Needless to say, I had a bit of a spell with this one. "What's that, you say I'm supposed to give money to the beggars? Oh shit man, I've been killing them instead!".

Yeah, whoops. Still, it was the best "boss battle" I've ever faced. And the battle lasted the entire game, at that. Top that. I dare you!

7. Save points are good - Many, many games of all shapes and sizes

Please, please, pretty please with sugar, whipped cream, a cherry, and three lines of cocaine on top, give me a save point before I take on a boss battle.

8. I want to finish your game. Really, I do - Pretty much any Psygnosis game ever, Data East c64 ports

Psygnosis was staffed by sadists. As developers, and publishers, they strove to provide the most unfair, ball-busting entertainment to be found on any platform. When you absolutely, positively, couldn't bear the thought of actually finishing a game you paid good money for, look no further! As a hidden bonus, the PC ports of their games were often harder than their Amiga counterparts. Baal, Stryx, Obliterator, Shadow of the Beast (any), Agony, Blood Money... the list is long indeed. Data East also provided much fodder for masochists with the c64 ports of their arcade games. These were largely impossible to beat by anyone who wasn't an idiot savant.

9. Difficulty should make a steady rise, not form a cliff or mountain - Drakkhen

Drakkhen was one of those rare games that fucked me so hard I just couldn't get enough, even when I was bleeding out both ears and missing half of my left asscheek. The game was designed to eliminate your party in under three minutes of starting a game. Normally you wouldn't survive you first random encounter, and even if you did there were numerous game-ending monsters lurking nearby to finish the job. Every enemy in the game was present and ready to rumble at the very start of the game, so you were frequently beset by enemies that could wipe out your party in a single hit. For most of the game, survival is quite a chore... so much so that I'd wager most people didn't get beyond the game's initial few minutes before tossing it in the garbage. To add insult to injury, the PC version didn't come with a map, so you had to wander the map (and you started in a random location, too!) looking for safe harbors, but you would likely die before you found anything. It was a miserable game, but it looked so good (for its time) and featured some very cool effects, so I suffered many nights at its hands.
_________________
Ask not for whom the telephone bell tolls... if thou art in the bathtub, it tolls for thee.

Sorting Algorithms

Author: Bean
Subject: Sorting Algorithms
Posted: Sat Aug 21, 2010 12:45 am (GMT -8)
Topic Replies: 29

I'm sure most of you are familiar with one or two sorting methods. Here's a couple kickass videos that apply sound to various algorithms with a nice visual so you can see how each one works.

-Bean
_________________
Nuclear Playground | VholdR

Google does a PC (browser) app store

Author: PoV
Subject: Google does a PC (browser) app store
Posted: Wed Aug 18, 2010 9:25 am (GMT -8)
Topic Replies: 21

Your required reading for this:

http://www.1up.com/news/google-shows-future-browser-games

- 5% processing fee (you keep 95%)
- No approval process
- Launches October 2010 (US Currency Only)

Yarg! I need to dust off my Native Client Smiles port now... not to mention figure out how to bypass the stupid "No Canadians can Sell" problem. :|
_________________
Mike Kasprzak
Sykhronics Entertainment | Smiles (iPhone, Palm Pre, PC/Netbook, Nokia N900, Bada, WM), Smiles HD (iPad), ??? (2012) | Blog

Your Dream Game Scripting Language?

Author: xearthianx
Subject: Your Dream Game Scripting Language?
Posted: Thu Aug 05, 2010 3:11 am (GMT -8)
Topic Replies: 63

There's a lot of scripting languages out there. Games have come to use them extensively as the demand for interactive content expands, and blurs the lines between data and code. For simplicity, familiarity, and sometimes I'm sure pure laziness, game devs often pick off-the-shelf languages, such as Lua, Python, LISP, etc. But none of these are really geared toward making games. Even the languages that are written for and packaged with games and engines often feel like scaled-back general purpose computation languages with a few hooks into engine services, rather than a solution custom-built specifically for the two tasks a game scripting language is ostensibly meant to facilitate: very fast dynamic programming, and handling common game management tasks.

So what would the features of your dream game scripting language be? Here are a few loose guilde lines (not rules!) I think most of us can agree upon, to get us started:

Super easy to embed and interface with native types and functions - in both directions
Garbage collection is a must - a script is not the place to be juggling memory allocations (unless you're using it to manage memory pools for your C code)
Expressivity and succinctness trump runtime efficiency - the point is to program high level logic quickly; leave engine programming for compiled languages
Ease of use and simplicity trump comprehensiveness - if generics or diamond inheritance or switch statements make it harder to use, leave them out!
Games oriented, not engine oriented - you want the feature set to apply to managing games in general, not cater to a particular engine's data or functions
Interactive, dynamic access - tweak any value or function, anywhere, at any time without any recompilation step
Optional persistence across sessions - what good is it to tune in that elusive sweet spot value in-game if you lose your results when you exit?
Think outside the box - what are the best and worst things about languages you know, and how can you exploit this knowledge with zany, domain-specific constructs?

I have a slew of ideas for designing a scripting language that generally follows the above philosophy. I'll start posting them to this thread. But I want to know what kinds of unusual syntax and features you have always wanted (or never knew you wanted until you sat down to think about it). Like a Huffman encoding, the most common tasks should require the least typing. Ultimately, I think it would be super awesome to have a GDR scripting language that we can all use for our games, though I'm not sure how realistic that is for a lot of reasons. In the mean time, however, it is at least a useful and fun thought-exercise.
_________________
<earthian> why should I have to think? that's what the computor box is for
<madgarden> Yes, except computers can't think either. D'oh!
<madgarden> WE'RE SO FSCKED!

July 26 Downtime

Author: Bean
Subject: July 26 Downtime
Posted: Tue Jul 27, 2010 9:55 am (GMT -8)
Topic Replies: 2

Last night HostGator had one of those catastrophic moments that I'm sure all hosts/datacenters dread.
I'm not sure exactly what happened but they had about 50 servers go down. Apparently something happened with a building. http, databases, ftp, e-mail, everything was gone.

And once again HostGator proved to me why they fuckin kick ass.
Their techs went into emergency holy-shit mode and got things handled They also had a huge team of customer service people ready to explain things and assist their customers. And they were honest about it all. No PR bullshit. And these guys were responding to e-mails, phone and online live chat. How many times have you tried to use another company's live chat only to be greated with an error message or a "sorry were closed" message. This was 2am and HostGator had almost 40 reps on there!
It took then a few hours to do what a lot of companies would have spent days working on. The GDR database took a little longer but they got that fresh out of the oven too (so we didn't have to use one of my oldass backups).

Most of you probably didn't even know the site was down and that I was scrambling for solutions. And that's a good thing.
So this is just me doing a lil ass kiss for HostGator because I really haven't dealt with many companies as awesome as they are.

-Bean
_________________
Nuclear Playground | VholdR

Revitalizing Game Design

Author: xearthianx
Subject: Revitalizing Game Design
Posted: Mon Jul 26, 2010 10:41 am (GMT -8)
Topic Replies: 7

Thoughtful blog on the thematic rut of current game design trends. Of course, this will always be less of an issue in the indie scene, where large corporate concerns will have less of a limiting effect on plot and game mechanics. But the viewpoint he puts forward should be useful in pushing creativity that extra notch that might just mean the difference between obscurity and success.

http://www.gamasutra.com/blogs/ChristopherTotten/20100726/5636/The_Importance_of_Research_Getting_the_Best_of_Postmodern_Design.php
_________________
<earthian> why should I have to think? that's what the computor box is for
<madgarden> Yes, except computers can't think either. D'oh!
<madgarden> WE'RE SO FSCKED!

BSP info and tutorials

Author: xearthianx
Subject: BSP info and tutorials
Posted: Fri Jul 23, 2010 4:20 pm (GMT -8)
Topic Replies: 6

I am currently in a Computational Geometry / Geometric Algorithms course. I needed to to figure out a term project, and attached myself to someone who wanted to do Bounding Volume Hierarchies. After a bit of poking around, we realized that to a first approximation, there is zero information about some of the implementation details (google for "treepsila", I dare you!) Thus, I suggested we switch to BSP trees, for which there is TONS of information out there, and gigabytes of source code to reference if needed.

So my question: What are some exceptionally good websites, online tutorials, books (bonus points if it's available as a pdf), or open source software projects that might make the subject clear and easy to understand? The textbook covers the subject, but is generally rather dense, and their pseudocode style sucks pretty bad. Any links that you already know are legit and would save me from hours upon hours of trawling through braindead websites and inscrutable journal articles would be appreciated++.
_________________
<earthian> why should I have to think? that's what the computor box is for
<madgarden> Yes, except computers can't think either. D'oh!
<madgarden> WE'RE SO FSCKED!

The "Useful Dev Tools" thread

Author: Sirocco
Subject: The "Useful Dev Tools" thread
Posted: Wed Jul 21, 2010 7:23 am (GMT -8)
Topic Replies: 27

We don't have one of there already, do we? I searched...

Any way, this is the thread for letting folks know about cool dev tools you're come across. Work smarter, not harder!

Here's a few I've been using:

Kiwi Log Viewer - Freeware

This is a standard real time log file viewer. You fire up your program, then let this app monitor the log file, and it will automatically update and scroll as things change. Good for those times when you don't have a console window to push messages to.

CppCheck - Freeware (WIP)

I've talked about this briefly in a previous thread. It's a semi-functional program that steps through a C++ project and makes note of some obvious problems you may have that might slip past your compiler. Right now it's mostly good for picking up memory leaks and unused variables. It needs more work before I'd classify it as an essential app.

Diff Tool and WinMerge - Freeware

Diff Tool is a supremely lightweight and simplistic code difference comparison tool. That's all it does. If you want to do diff + merge, you need something like WinMerge instead. Meld looks interesting on the Linux side, but I can't attest to it as I'm not a Linux user at the moment.
_________________
Ask not for whom the telephone bell tolls... if thou art in the bathtub, it tolls for thee.

Android App Inventor

Author: Bean
Subject: Android App Inventor
Posted: Mon Jul 12, 2010 7:42 pm (GMT -8)
Topic Replies: 11

This looks like it could be good.

http://appinventor.googlelabs.com/about/

It might be awhile before I've got a chance to try it but it's definitely something I'm interested in. If anyone else messes with it, let us know how it is!

-Bean
_________________
Nuclear Playground | VholdR

Okay, it's time for the talk.

Author: Ninkazu
Subject: Okay, it's time for the talk.
Posted: Sat Jul 03, 2010 11:00 am (GMT -8)
Topic Replies: 45

There are those of you who swear by C/C++, maybe Java or Python. I'm starting this thread to introduce a new possibility. Not necessarily a new language, but an overlooked paradigm.

Functional programming.

This is a long post that's split into different sections. Feel free to peruse.
1. Correctness of Programs
2. Proof of Correctness
3. I Don't Like Math - Is Functional Programming Still For Me?
4. List Processing Axioms

I bring this up because of my experience in theorem proving and research in programming languages. So many cool ideas have been introduced by academia in the past 25 years that still go unnoticed because people want their pointer arithmetic.
Pointers, as you all must know, 99.9% of the time they're used, cause headaches, rage and bugs. I'm not going to say they're not useful tools when used "right," but they cause so much non-local behavior that reasoning about correctness of your program becomes an exercise of futility. What correctness means for C/C++ users, I don't know, since there is no such thing as C/C++ - just the idea. Compiler bugs mean new dialects of these languages. Their type system is claimed "weakly typed," but really that just means it's unsound. Types mean nothing in these languages.
Please, if you have a disciplined use of pointers, post about it so we may engage in a discussion about alternative safer methodologies.

That aside out of the way, I've found that my experience with functional programming has made me much more aware of writing stateful code. You know the pervasive assignment statements in imperative code? Most of the time they're unnecessary. They introduce the need for whole-program analysis to ensure proper behavior. Recursion is such a powerful tool that makes assignment almost unnecessary, and its mathematical basis is so closely linked with (structural) induction that reasoning about your code becomes much more straightforward.

Allow me to demonstrate. Let us first discuss what correctness means.
Correctness of Programs
For pure (assignment-free) functional programs, functions are actual functions f(x) will always be the same value for every call. This means we can write simple (if inefficient) programs that we can agree are "correct by inspection," and then prove our more efficient version produces the same values. This is what is called "functionally equivalent."
If we instead are trying to model a data structure, we can write a simple version and our "better" version and come up with a map from one to the other. What must then be proved is that each interface after a change produces the same value. This is called "observational equivalence." This is a little more complex, so here is an example:

First the simple implementation of a queue. True-listp means a chain of conses that end in NIL, e.g. (cons 1 (cons 2 (cons 3 nil))) = (list 1 2 3). The convention in LISP of adding "p" means that the function is Boolean, i.e. a predicate.
Those of you unfamiliar with languages that have lists should refer to the end of this post where the behavior of each function is described axiomatically.

Abstract implementation:
This models a queue as a list whose front is the beginning of the list, and whose back is the end of the list. Enqueueing means a linear operation. Slow. Enqueueing and dequeueing return modified copies of the queue that you would then use.

Code:

(defun queue-absp (q)
(true-listp q))
(defun enqueue-abs (e q)
(append q (list e)))
(defun peek-abs (q)
(car q))
(defun dequeue-abs (q)
(cdr q))
(defun emptyp-abs (q)
(null q))
(defun newqueue-abs ()
nil)

Complex implementation:
This implementation is two lists. The first list is the enqueue list and the second list is the deque list. They are managed in the opposite order. Given a balanced spread of enqueues and dequeues, interaction is constant time.

Code:

(defun queuep (q)
(and (consp q)
(true-listp (car q))
(true-listp (cdr q))))
(defun enqueue (e q)
(cons (cons e (car q))
(cdr q)))
(defun dequeue (q)
(if (null (cdr q))
(cons nil
(cdr (reverse (car q))))
(cons (car q)
(cdr (cdr q))
(defun peek (q)
(if (null (cdr q))
(car (reverse (car q)))
(car (cdr q))))
(defun newqueue ()
(cons nil nil))
(defun emptyp (q)
(and (null (car q))
(null (cdr q))))

Map between the two:
(defun abs2complex (q)
(cons nil q))
(defun complex2abs (q)
(append (cdr q) (reverse (car q))))

The theorems that must hold (free variables are universally quantified):
(implies (queuep q)
(equal (emptyp q)
(emptyp-abs (complex2abs q))))
(implies (queuep q)
(queuep-abs (complex2abs q)))
(implies (queuep q)
(equal (enqueue e q)
(enqueue-abs e (complex2abs q))))
(implies (and (queuep q)
(not (emptyp q)))
(equal (dequeue q)
(dequeue-abs (complex2abs q))))
(implies (and (queuep q)
(not (emptyp q)))
(equal (peek q)
(peek-abs (complex2abs q))))
(equal (complex2abs (newqueue))
(newqueue-abs))

And conversely with abs2complex and reversing the use of complex and abstract forms.

There are more complicated notions of correctness that I won't go into here, but if you're interested seek "refinement maps."
I will talk about one more, and that is correctness by constraint, or properties that must hold.
Consider what it means for a sorting algorithm to be correct. Actually for sorting, that turns out to be ambiguous due to the notion of stability (and order). Let us then consider a simpler domain - what does it mean for an ascending sort of integers to be correct?
Is it.. that the sort produces an ordered list? Let's define ordered list:

Code:

(defun orderedp (lst)
(if (and (consp lst)
(consp (cdr lst)))
(and (<= (car lst) (car (cdr lst)))
(orderedp (cdr lst)))
T))

This function says empty and singleton lists are sorted. If you're a list of 2 or more elements, your first element has to be less than or equal to your second element. We continue this down the line until the end.
That sounds reasonable, right?
Well then:

Code:

(defun amazingsort (lst)
(list 1))

Is a correct sort. Er, not what we wanted. Oh ya, the lists have to have the same elements. Not only that, they have to have the same number of occurrences of each distinct element. Well that's just a permutation.

Code:

(defun permutationp (lst1 lst2)
(cond ((atom lst1) (atom lst2))
((atom lst2) NIL)
(t (and (in (car lst1) lst2)
(permutationp (cdr lst1) (delete1 (car lst1) lst2))))))

(defun in (e lst)
(if (consp lst)
(or (equal e (car lst))
(in e (cdr lst)))
NIL))

(defun delete1 (e lst)
(if (consp lst)
(if (equal e (car lst))
(cdr lst)
(cons (car lst) (delete1 e (cdr lst))))
lst))

That's a lot to think about, even for stateless programs. At least I can prove that insertion sort is a real sort.

Proof of Correctness
Now most of you guys I'm sure are used to the more test-based methodology of ensuring (actually, convincing yourself of) correctness of your programs. You can't test /every/ input though. You can however use mathematical tools to prove that your program behaves how you mean it to under every possible input. What I'm about to show you is long and tedious, but guess what? It's so mechanical that there actually are mechanical theorem provers out there that can do this for you.

Let's say I want to prove insertion sort is correct. Let's start with a definition.

Code:

(defun insert (e lst)
(if (atom lst)
(list e)
(if (<= e (car lst))
(cons e lst)
(cons (car e) (insert e (cdr lst))))))

(defun isort (lst)
(if (atom lst)
lst
(insert (car e) (isort (cdr lst)))))

Okay, so what do we want to prove here? First (orderedp (isort lst)) and next (permutationp lst (isort lst))

Code:

By induction on the definition of isort, we must prove these two obligations:
1. (implies (atom lst)
(orderedp (isort lst)))
2. (implies (and (not (atom lst))
(orderedp (isort (cdr lst))))
(orderedp (isort lst)))

1. Hypotheses:
H1) (atom lst)

(orderedp (isort lst))
= {definition of isort, H1}
(orderedp lst)
= {definition of orderedp, H1}
T

2. Hypotheses:
H1) (not (atom lst))
H2) (orderedp (isort (cdr lst)))

(orderedp (isort lst))
= {definition of isort, H1}
(orderedp (insert (car lst) (isort (cdr lst))))
= {insert is order-preserving / e = (car lst), x = (isort (cdr lst)), H2}
T

That last step needs to be justified. What's e? What's x? They're the universally quantified (and thus I may instantiate them) variables in the "insert is order-preserving" lemma I will now prove.
(implies (orderedp x)
(orderedp (insert e x)))

Code:

By induction on insert, I must prove
1. (implies (and (orderedp x)
(atom x))
(orderedp (insert e x)))
2. (implies (and (orderedp x)
(not (atom x))
(<= e (car x)))
(orderedp (insert e x)))
3. (implies (and (orderedp x)
(not (atom x))
(not (<= e (car x)))
(orderedp (insert e (cdr x))))
(orderedp (insert e x)))

1. Hypotheses:
H1) (orderedp x)
H2) (atom x)

(orderedp (insert e x))
= {definition of insert, H2}
(orderedp (list e))
= {definition of orderedp}
T

2. Hypotheses:
H1) (orderedp x)
H2) (not (atom x))
H3) (<= e (car x))

(orderedp (insert e x))
= {definition of insert, H2, H3}
(orderedp (cons e x))
= {definition of orderedp, H1, H2, H3}
T

3. Hypotheses:
H1) (orderedp x)
H2) (not (atom x))
H3) (not (<= e (car x)))
H4) (orderedp (insert e (cdr x)))

(orderedp (insert e x))
= {definition of insert, H2, H3}
(orderedp (cons (car x) (insert e (cdr x))))
= {definition of orderedp, insert is a cons lemma}
(and (<= (car x) (car (insert e (cdr x)))))
(orderedp (insert e (cdr x))))
= {H4, propositional logic}
(<= (car x) (car (insert e (cdr x)))))

[Okay there are a couple things that could happen here. Either e is the first in the inserted list or not. We consider both cases]
Case 1: (equal (car (insert e (cdr x))) e)
(<= (car x) (car (insert e (cdr x)))))
= {Case hypothesis}
(<= (car x) e)
= {H3}
T

Case 2: (not (equal (car (insert e (cdr x))) e))
(<= (car x) (car (insert e (cdr x)))))
= {definition of insert, insert is a cons lemma}
(<= (car x) (car (cons (car (cdr x)) (insert e (cdr (cdr x))))))
= {car/cons axiom}
(<= (car x) (car (cdr x)))
= {H1, definition of orderedp}
T

The insert is a cons lemma is easily shown by case analysis (every if branch returns a cons), so I won't show that proof.

The next theorem to prove is (permutationp lst (isort lst)), which is a little trickier.

Code:

By induction on permutationp, we have the following obligations
1. (implies (atom lst)
(permutationp lst (isort lst)))
2. (implies (and (not (atom lst))
(atom (isort lst)))
(permutationp lst (isort lst)))
3. (implies (and (not (atom lst))
(not (atom (isort lst)))
(permutationp (cdr lst) (delete1 (car lst) (isort lst))))
(permutationp lst (isort lst)))

It looks like I need to prove a connection between (atom (isort lst)) and (atom lst), but this is simple so I'll just refer to this lemma:
(iff (atom lst) (atom (isort lst)))
as isort-cons-preserving

1. Hypotheses:
H1) (atom lst)
(permutationp lst (isort lst))
= {definition of permutationp, H1}
(atom (isort lst))
= {definition of isort, H1}
T

2. Hypotheses:
H1) (not (atom lst))
H2) (atom (isort lst))
From these hypotheses I can derive NIL {isort-is-cons-preserving}, so since false implies anything, this is T.

3. Hypotheses:
H1) (not (atom lst))
H2) (not (atom (isort lst)))
H3) (permutationp (cdr lst) (delete1 (car lst) (isort lst))))

(permutationp lst (isort lst))
= {definition of permutationp, H1, H2}
(and (in (car lst) (isort lst))
(permutationp (cdr lst) (delete1 (car lst) (isort lst))))
= {H3, propositional logic}
(in (car lst) (isort lst))
= {in-isort-lemma}
T

Again we have an inductive lemma we need to prove to wrap this up: (in x (insert x y))

Code:

Induction on insert gives us these obligations:
1. (implies (atom y)
(in x (insert x y)))
2. (implies (and (not (atom y))
(<= x (car y)))
(in x (insert x y)))
3. (implies (and (not (atom y))
(not (<= x (car y)))
(in x (insert x (cdr y))))

1. Hypotheses:
H1) (atom y)

(in x (insert x y))
= {definition of insert, H1}
(in x (cons x nil))
= {definition of in, reflexivity of equal}
T

2. Hypotheses:
H1) (not (atom y))
H2) (<= x (car y))

(in x (insert x y))
= {definition of insert, H1, H2}
(in x (cons x y))
= {definition of in, reflexivity of equal}
T

3. Hypotheses:
H1) (not (atom y))
H2) (not (<= x (car y)))
H3) (in x (insert x (cdr y)))

(in x (insert x y))
= {definition of insert, H1, H2}
(in x (cons (car y) (insert x (cdr y))))
= {definition of in, H3, propositional logic}
T

And thus insertion sort indeed sorts. Some of those lemmas I came up with aren't necessary to prove in mechanical systems because they're easy enough to get. Nifty stuff.

I Don't Like Math - Is Functional Programming Still For Me?
Awww, you don't like math? They beat it out of you as a kid I'm sure. Math is great.
Not convinced? Well let me demonstrate the beauty of higher-order functions and macros not as mathematical wonders, but as tools to arbitrarily shorten the length of your programs - making them easier to write, read and understand.
Before I begin, I will say that Google is able to do much of their cloud computing because of the paradigm of higher order functions. Perhaps you've heard of "MapReduce?" Both map and reduce are pervasively used higher order functions. Here is what they do.

Map is a function that takes a function f, and a list X. It returns the list with f applied to each element of X, in the same order (thus f must be unary). That's it, but it's very powerful.
Reduce accumulates results of a map using an accumulator function of your choice. Here are their definitions

Code:

(defun map (f X)
(if (consp X)
(cons (f (car X)) (map f (cdr X)))
nil))

(defun reduce (f acc base X)
(if (consp X)
(acc (f (car X)) (reduce f acc base (cdr X)))
base))

There are so many things I can do with these guys. Let's redefine in from the permutation example:

Code:

(defun in (e X)
(reduce (lambda (x) (equal e x)) or nil X))

Lambda here is a way to create nameless functions - you don't have to use defun if you don't want to*.

Macros in Scheme, a LISP-like language
Macros are actually a hot area in programming language research. "Hygienic" macros are far more complicated than LISP or C macros, which are really just textual replace algorithms. Entirely unsafe stuff.
Consider a C macro for swap:

Code:

#define swap (x, y) {int temp = *x; *x = *y; *y = temp; }

So what happens if I do this?

Code:

int updateTemperature(int *temp) {
swap(temp, g_oldtemp);
}

This expands out to

Code:

int updateTemperature(int *temp) {
{int temp = *temp; *temp = *g_oldtemp; *g_oldtemp = *temp; }
}

Luckily here the compiler would complain, trying to dereference an int, but normally you wouldn't be so lucky.
Hygienic macros preserve lexical scope from where you defined your macro. I won't go into the specifics of how it does this, but it's really nifty.

Code:

(let ((x "outside"))
(let-syntax ((m (syntax-rules ()
((_) x)))
(let ((x "inside"))
(m))))

This expands into

Code:

(let ((x1 "outside"))
(let ((x2 "inside"))
x1))

Which is great - we wanted m to refer to the x that was in scope when we defined it. This syntax-rules thing is a transformer function that allows you to enter high-level pattern specifications for your macros - no mucking about with consing symbols everywhere (see the list macro below).
Consider a language with lambda but no let. I can define let this way

Code:

(let-syntax ((let (syntax-rules ()
((_ ((id expr) ...) b ...) (lambda (id ...) (begin b ...)) expr ...))))
...rest-of-program...)

Neat stuff. Now, if you want to do arbitrary syntax generation without being bound to this pattern language, you can! And there's a hygiene story for that as well. You don't even have to give up the nice abstraction tools that syntax-rules gives you.

Code:

(let-syntax ((primer (lambda (stx) (syntax-case stx ()
((_ number ...) (if (reduce (lambda (x) (prime? x)) and #t number)
(syntax number ...)
(raise-syntax-error "Failure! Only primes damn it!")))))
...)

You may have caught on that hygiene restricts you from referencing variables not in scope. Well, you can get around that. Hygienically.
First, let's implement a simple version of cond, which is basically a chain of ifs compacted into a nice form.

Code:

(letrec-syntax ((cond (syntax-rules (else)
((_ (test result ...) . clauses) (if test (begin result ...) (cond clauses)))
((_ (else result ...)) (begin result ...)))))
...)

The else in the parentheses means that else should not be considered a pattern variable, but a literal to match against. If you rebind else in your code, then it won't match with the cond else and you'll get a syntax error.
Say you want to have an if where the result of the test is available to you as the variable "it." It has a value, and it will be in your result code, so you can't just say it's a literal to match against. Here's what you do.

Code:

(let-syntax ((ifit (lambda (stx) (syntax-case stx ()
((_ test then else) (with-syntax ((it (datum->syntax (syntax then) 'it)))
(syntax (let ((it test))
(if it then else))))))))
; test code:
(if 3 it #f))

Pretty sweet huh? datum->syntax can introduce identifiers into whichever lexical scope you want by giving it the corresponding syntax object.
By building up these syntactic abstractions, you can eliminate boilerplate code in your programs (say a complicated initialization sequence) and solve problems in the notation you want to solve them in. These macros can be arbitrarily complex, and our understanding of how to prove properties about them is extremely limited (normally you completely macro-expand before you start proving theorems in these mechanized theorem provers).
My research is focusing on how to allow reasoning about macros so you can prove semantics-preserving program transformations correct, instead of having to prove in each instance of their use that the resulting code is semantically equivalent to the macro's input.

I know this post is long, and I kinda skimped on details close to the end, but I hope this conversation will continue so I may expand on what great possibilities there are in functional programming languages.

List Processing Axioms

Code:

(car (cons x y)) = x
(cdr (cons x y)) = y
(consp (cons x y)) = T
(atom x) = (not (consp x))
(implies (consp x)
(equal (cons (car x) (cdr x)) x))
(null NIL) = T
(null x) = NIL (if x <> NIL)
(if NIL x y) = y
(if w x y) = x (if w <> NIL)

(append x y) =
(if (consp x)
(cons (car x) (append (cdr x) y))
y)

(reverse x) =
(if (consp x)
(append (reverse (cdr x)) (list (car x)))
nil)

defun means "define function."

(list x) = (cons x nil)

Actually, list is a macro, which means it takes arbitrary syntax and expands into core syntax. Here is the full definition of list.

Code:

(defmacro (list &rest args)
(if (consp args)
(cons 'cons
(cons
(car args)
(cons (cons 'list (cdr args))
nil)))
nil))

This is a recursive macro definition. In LISP, this is generally discouraged since macro expansion tends to be slow. A better implementation would call a function that would generate the complete list syntax for the macro to "reify" (turn from a list of symbols into accepted syntax). This close connection between programs and data is what makes LISP-like languages so powerful.

In LISP, NIL stands for false and the empty list. This paradigm has since been rejected with newer LISP-like languages.

* In this example I glossed over the fact that or is a macro that can take any number of arguments. Macros cannot be passed around like functions in most languages, so think of this or as (lambda (x y) (or x y)).
_________________
The one true Ninkazu.