Wednesday, December 17, 2014

Syntax Matters

Originally, I didn’t worry too much about programming language syntax.  I think, starting out, I simply didn’t have enough exposure to the different options.  Then as I started to really get interested in programming languages, my interest was focused on the semantics of different features.  How they looked didn’t seem to make any difference when I had no idea what they actually did.  Lisp and Forth were probably my first clue that syntax would be significant.  And that makes sense because in those languages the syntax allows certain constructs to exist.  However, I think that even if there does not exist any language construct that necessitates a specific syntax, the syntax of your language still has effects.

In Let Over Lambda [1], Doug Hoyte talks about “Duality of Syntax”.  I’m not going to go into detail of this concept, but I believe he uses this principle in order to justify deviating from typical common lisp conventions as well as deciding on how to design new conventions.  This is important because it’s setting up a theory on what makes good programs and then makes decisions in that framework.  

You also see this (but sort of in the other direction) with Douglas Crockford’s Javascript the Good Parts [2].  And the punchline is something that I talked about in a previous blog post [3].  Normally, where you put a curly brace doesn’t really matter, but in javascript it does matter because semicolon insertion means that a return statement for an object literal might instead return ‘unknown’.  Douglas’ solution is to say that in javascript you always put the open curly brace on the same line because that way you won’t run into the semicolon insertion problem.  Here we’re using a syntax convention in order to avoid bad parts of the language, but my thought is that we should observe situations like what has occurred with javascript and instead create new languages that do not have these defects.

Also observe Jonathan Blow’s video series for the new programming language that he is developing [4].  Specifically try to keep an eye out for how he’s designing the syntax for functions.  A locally defined function has nearly the exact syntax as a globally defined function; that’s on purpose.  This design decision allows for a work flow that is much better optimized than if local and global functions have different syntaxes.  

And finally take a look at my previous blog post [3] where I propose that we can decide what good syntax is by determining if it possesses certain mathematical properties that are advantageous.

Now I don’t think that there is going to be a ‘one syntax to rule them all’, but I do think that the reasoning behind our syntax and conventions needs to be based off of what properties we want our code to have.  Just choosing an arbitrary set of rules for the sake of uniformity is missing the point (although it’s clearly on the right track).  What we need is a careful analysis so that we can show in a very methodical fashion that our rules are helping us and not hindering us.

Wednesday, December 10, 2014


The indie game developer Jonathan Blow is currently trying his best to create a replacement for the C programming language with the intended use case of developing games (go figure).  In general I think that replacing C/C++ is a good call; my personal belief being that undefined behavior [1] is a bigger problem than the college lectures let on.  And honestly, replacing C/C++ seems to be en vogue these days [2].  

Now Jonathan’s project is still a work in progress, but he’s racked up quite the impressive length of video digression into this subject [3].  If you watch through those videos, you’ll get the impression (and part of this comes from explicit statements) that the goal of this language is to be an 85% language.  Fix the parts of C that are rather archaic, optimize for the use cases that game designers care about, avoid syntactic and semantics pitfalls that do not have any reason to exist and we can fix with zero cost, but don’t ground the thing in whatever crazy lambda calculus the cool kids are playing with this decade.  After all we would like to be able to get some work done by Thursday without having to learn category theory in order to do it.

I think that the 85% goal is a pretty good one if you already know how you want to be programming.  If your patterns stay the same and are always doing *basically* the same things, ensuring that weird edge cases fit into your system might actually be a waste of time.  You can handle those issues with code reviews, stack traces, and debuggers.

However, on the other hand, my personality doesn’t get along with very well with 85% solutions.  Economically, I see why they are absolutely necessary, and I wouldn’t hesitate to use an 85% solution as an implementation detail if my focus is on whatever the bigger picture is (assuming of course the 85% can be verified to fully satisfy the requirements).  But if my goal and focus is to understand the thing (whatever it is), I’m going to lean towards 100% solutions nearly every time.

I think the reason for this is because my learning style seems to involve some sort of combination of counter example search and backtracking.  Break everything apart into the smallest pieces you can and then try to put the pieces back together again.  Anytime you think you have a semantic meta statement look for counter examples.  If you find a counter example then something is wrong, so backtrack until you can’t find any counter examples.  Once you can’t find any counter examples for anything you’re done.  Not quite a proof of correctness, but success by exhausting all avenues of failure seems like it ought to work better than “but this worked last time”.

Here comes the punch line:  I’ve already mused about mathematical properties being valuable for programming correctness [4].  And I think the reason for that is because the context of a property is 100% (and by the way we have proofs).  You don’t have to worry about things going wrong tomorrow.  I think the reason that we need to be replacing C/C++ today is that they were the 85% languages of yesterday.  The programming techniques we’ve developed just don’t fit into languages that were developed in a very different environment.  Maybe you want an 85% solution or programming language because you need to get work done today and you don’t want to worry about proofs of correctness.  And maybe that’s going to work.  On the other hand maybe someone will misuse your solution or new techniques will arrive that can’t be safely utilized in your language.

[2] - Microsoft is supposedly developing *something*, Apple has developed Swift, Mozilla is developing Rust, Facebook seems interested in D, Google has developed Go, the C++ standard is trying to modernize.

Tuesday, December 2, 2014

Compiler : Syntax -> Program

It has seemed to me for a while now that the significant whitespace in languages like F#, Haskell, and Python is actually a really good thing.  After all, correctly formatted code already has indentation delimiting scope.  And there exist compilers that will correctly compile code that has significant whitespace (i.e. F#, Haskell, Python).  Conclusion:  Curly brackets et al are all only to make the compiler writers’ life easier, the right way to delimit scope is with significant whitespace.

However, one of the more horrifying things that I’ve encountered in programming languages are the bizarre errors that can occur from Javascript’s semicolon insertion.  Basically, the problem is that:

return {
    a : b

is different from 

    a : b

The first one returns an object that has a field ‘a’ with a value ‘b’ and the second one returns ‘undefined’.

Why is semantic whitespace in the same post as javascript semicolon insertion?  Because I realized that they both share the same property (or lack thereof).  Both are discontinuous.  

The title to this post is actually an indirect reference to my previous post [1].  In that post I said that there are a bunch of mathematical properties that we really should make sure our programming constructs have (for example … some constructs really should be continuous).  *This* post is about how compilers are really just functions that map syntax into programs.  

The gist behind continuous functions is that a small change in the input should result in a small change in the output [2].  The problem with the javascript example is that a small change in the input (a single invisible character that only changes formatting and almost never has any semantic value in other languages) will result in a very large change in the resulting program semantics.  If you accept that this is a problem in javascript it seems like you have to also accept that this is a problem in languages like python (a single invisible character that only changes formatting has non-trivial semantic results).

The thesis here is that a continuous compiler is good and a discontinuous compiler is bad.  One solution might be to add in curly braces and remove semicolon injection … but I suspect there may be better ways to salvage the situation.

ReSharper is a neat add-on to Visual Studio that adds a bunch of additional syntax highlighting (among other features).  One of the things I’ve really enjoyed is the grey out effect that occurs when a function is not called anywhere.  It becomes rather easy to determine at a glance when a function has become obsolete.  And I suspect that this is also the answer to solve the semantic whitespace discontinuity.

The only real problem I have is that I want a continuous syntax to semantic mapping.  So if I can convert the small change we see with semantic whitespace into a big change then the problem should be solved.  If we take a page from ReSharper, then we can change the color scheme slightly (maybe only a tint change) when the scope of an expression is different.  Each scope can have a different tint and then the small change causing a large differing output will be converted into a noticeable change causing a noticeable differing output.  Additionally, this technique could also be leveraged to address some of the issues with semicolon insertion in javascript.

[2] - Things get complicated when you aren’t dealing with geometry or metric spaces.  What do you mean by “small change” when distance doesn’t exist in your domain?  Well, topology has a solution for that, but I’m not going to try to build a topological space for syntax and program semantics.  I think the informal ideas for small change is clear enough to get the idea in this instance.

Sunday, November 30, 2014

Mathematical Properties and Programming

In school part of the maths education involved memorizing the definitions for words like “commutative” or “transitive”.  I always did terrible with those memorizations [1], however I’m pretty sure the cause behind my performance was a lack of context.  Trying to investigate maths on my own, I reencountered these words.  My first thought was something along the lines of, “hey these are those words I always missed points on with exams.”  However, I wanted to understand certain maths [2], so I trudged on.  I’m rather glad I did because an important realization struck me once I had finally memorized enough of these definitions:  If you create a programming construct [3] that does not obey a property that it should intuitively have, then when you (or someone else) uses the construct in the intuitive fashion it may malfunction in surprising or hidden ways.

The example that first comes to mind is floating point numbers in most programming languages.  Typically we imagine addition to be associative.  That is to say that a + (b + c) is equal to (a + b) + c.  However, this is not necessarily true for the floating point representation of a number [4].  The effect is that apparently valid looking code that uses floating point numbers may be incorrect, and apparently innocent looking code changes to code that uses floating point numbers may result in correct code becoming invalid.

Of course this doesn’t just apply to programming constructs that are baked into your programming language as a base feature.  It also applies to pretty much any class, object, inheritance chain, function definition, etc that you might end up creating in order to accomplish your goal. 

So far I’ve compiled a list of properties that look like that are important to keep in mind when you’re implementing solutions:

Equality Relation (reflexive + symmetric + transitive)
Partial Order (reflexive + antisymmetric + transitive)
Unary / Binary Idempotence 
Continuous (in the topological sense)
Monotonic (in the domain theory sense)
Continuous (in the domain theory sense)
Sound (in the type theory sense)
Referential Transparency

Not all of these properties are going to be required (or even a good idea) for every construct you come up with.  But when you’re using a construct like it has one of these properties it better have that property.

[1] - Actually I tend to *do* terrible with all memorizations, but that’s a different story.
[2] - Type theory and category theory (mostly because of Haskell).
[3] - It’s so much worse than just programming constructs though.  It also applies to reasoned arguments, personal philosophies, business procedures, school policies, and the list goes on.

Saturday, November 1, 2014

Competency categories

In my previous post [1] I mentioned wanting to have a better idea of how people think different.  I initially started down this road because neither of the descriptions for extrovert or introvert really seemed to describe me very well.  Different people seem to explain the way these personality types are different in different ways, but none of them really stuck when I tried to apply them to myself.  Well, that's okay because no one is really 100% introvert or 100% extrovert, except for *weird* people, most fit someplace in the middle.  But that's just the thing.  I don't feel  like I'm in the middle of extrovert and introvert.  And I don't seem to be on one extreme or the other.  I feel that I tend towards the extremes of both.  Instead of the introvert/extrovert scale being a line with two opposite ends, it feels more like maybe it's a circle where being "in the middle" might also mean being diametrically opposed to yourself.

My secondary foray into people being different occurred because I noticed some anomalies with my software development career, and the way I approach playing certain games is a bit peculiar.  

Concerning software development, I've noticed that there are certain people who I work shockingly well with, but terribly bad for.  There's a significant distinction here.  Working with someone suggests a collaborative process where each person covers the shortcomings of the other and working for indicates someone proclaiming and verifying goals with someone else doing the actual work.  Okay quick digression into games.

I've noticed that I really like to build decks in the card game Magic the Gathering [2].  Additionally, my actual strategies during play are entirely decided ahead of time during deck construction.  The actual play time strategy could be considered greedy.  Play all land, summon as many creatures as you can, attack as much as you can.  Maybe some finer points if some additional information is present or if there's a social element at play in a >2 player game, but basically a python script could do about the same thing.

Additionally, my ability to make any progress with RTS games like Supreme Commander [3] just isn't that up to scratch.  My ability to deal with keeping resources sane while also adapting to a dynamically changing battle field really isn't that good.  Although on the other hand analysis ahead of time concerning what units have good strategic value is something I can actually do.

So what's the deal?  My thought was that maybe there's two ways people can think.  Or deal with situations might be a better way of saying it.  There's observation and there's actualization.  Additionally, with these two modes there's a spectrum for each ranging from analysis to action.  In this system I would be a heavily leaning action person in the actualization mode and someplace in the middle for the observation mode (but closer to analysis).  The theory is that when actually playing the game my actions are primitive, but ahead or after observation allows more strategy.  To be better at an RTS, you would expect someone's actualization to be more balanced.

Back to software development.  If I'm working with someone who has a balanced actualization mode of thinking and an observation mode that is skewed towards action, then I can give up any actualization on my own and focus completely on observation.  The only actions I have to perform are simple social prods that keep development going in a direction that I've already worked out is viable.  They don't have to worry about category theory and I don't have to worry about implementing certain things I find frustrating. 

This would also explain why I don't work "for" these sorts of people very well.  My actions aren't nearly as graceful as they would prefer and meanwhile I don't like it that they can't actually explain what they want done and instead focus on how I didn't do what they imagined.

Now my most recent approach to this problem is what I indicated in my previous post combined with the actualization vs observation thing.  Instead of having a spectrum for actualization and observation you substitute in cognitive complexity classes [4].  So maybe the best actualization you can handle is a certain level of complexity and the best observation you can handle is on a different level of complexity.  This sort of thing seems to explain how there are very clever people who don't appreciate how clever they are (they tend to have a hard time understanding how people aren't as clever as they are) and get into trouble when their reach exceeds their grasp.  In other words if you can handle very high complexity for actualization you can accomplish very cool things (like writing operating systems or graphic renderers effortlessly).  Although if you can't handle very high complexity for observation maybe you don't have an appreciation of how hard the thing you're doing is or maybe your theoretical grasp on the whole thing is suspect (the cowboy coder whose codebase is a horrifying collection of hacks, but it somehow works nearly all of the time).

Unfortunately, I'm pretty sure right now that cognitive complexity classes don't yield a convincing or coherent picture when merged with observation vs actualization.  Too many things aren't falling into place when it looks like they should and there's also a bunch of things it doesn't explain.

It seems kind of like being competent at something means you can handle high complexity.  And then the categories of things you can be competent in is this huge set of things that's interrelated in weird ways.  So for example, macros, very higher order functions [5], and type theory are all things that don't bother me.  However, for loops and if statements not so much.  Judo, walking on uneven terrain, and public speaking:  yes.  Parties, interactive self expression, and relationships:  no.

A lot of this stuff sounds kind of good, but it seems sort of like the situation is a lot more complicated than being able to divide the world into halves again and again.  So instead of nice points on a coordinate plane or vectors or whatever, we end up with a messy graph that describes each person, each weight being another messy graph.  At the very least handling complexity and competence look vaguely related, so maybe I'll think in that direction for a while.

[1] -
[2] -
[3] -
[4] -
[5] - Functions taking functions that take functions that return functions that return functions.

Thursday, September 11, 2014

Analysis, Actualization, and Perfect Functionality

I’ve noticed that I have a much better time analyzing how code works than I do actually writing out code.  This actually touches on several different ideas that I’ve had in the past.  Cognitive complexity classes [1] so far haven’t turned out to be any sort of overreaching “this is what problems really are” concept, but it might be a good way to describe how people approach, solve, and understand problems.  Additionally, I have some ideas about the different ways in which people try to understand and mutate the world that I haven’t published.  Looks like I’m going to have to do a write up about that soon.  But the end game is an expounding on how people are different and why that makes writing software hard that I initially wrote about in [2].

It seems like it’s going to take a while to write everything up, but I’ve got a couple of things I want to get out here to start with.  I’ll go back and fill in all the details that led up to this later.

Analysis is easier for me than actualization.  And it’s something along the lines of I can analyze arbitrarily complex things and I enjoy the process, but when it comes to performing an action (like coding up some functionality) I want everything to be very simple.  This has caused me problems with my interest in parsers because parsers are kind of complex.  Unless you use monadic parsers.  Monadic parsers are pretty simple to use, but require either understanding category theory or a lot about how lambdas and higher order functions work (or maybe a little of both).  So I guess my point is that if I want to do something complex, I want to be using sub lexical scope injecting, dependently typed macros.  And that’s kind of weird.  Also this isn’t a “use cool new hip features because I’m a rockstar” type of thing.  This is a “I can keep the type system, macro expansions, meta object assignments, and higher order anonymous functions straight in my mind, but I’ll take a cheese grater to my face if I have to deal with passing a widget to that function after assigning three properties magic numbers in the right order and calling init on the ‘unrelated’ foofactory” type of thing.  Hopefully a better explanation will be forthcoming in blog posts yet to come, but for now…

Three Steps For Writing Functions that Never Fail*

1) Always write functions that are obviously total

2) If the function can’t be total, write a DSL that generates correct inputs for the function.  Only ever use the DSL and all inputs will be correct by construction.

3) If you can’t write a DSL because the inputs to the function come from some outside source (or some other situation prevents it), run all inputs through a parser to verify that the inputs are valid for the function.  Use a monadic parser composed of a bunch of simple obviously total functions and monadic combinators that form a correct by construction DSL.  If at any point anything becomes too complex recursively follow these rules.

I don’t know if all interesting programs can be written following this strategy (or even the smaller set of all programs *I’m* interested in), but I’ll see if I can’t look into that and write a follow on blog post focusing on that question.

* - This process seems like it should work for me.  Unfortunately, this gets into ‘people are different’ territory and we’ll have to wait until later for a digression into that.

Wednesday, August 6, 2014

two three one

The Feynman problem-solving algorithm was a joke that Murray Gell-Mann [0] made in order to talk about the seemingly magical way Richard Feynman came up with solutions to problems (a trait that was noted by more than one person [12]).  The algorithm works like this:  1) write down the problem, 2) think very hard, 3) write down the solution.  While I think the reason why this is a joke is pretty obvious, the frustrating thing is that occasionally this is the only honest way to proceed with solving a problem.  Looking back on the landscape of dead ends, blind alleys, and failed techniques, the victors are forced to concede that the answer really did come from the 20 minute break when they went off to grab some yogurt.  The solution came from a process that was not only non-continuous, but actively disjoint from as far as anyone can tell the rest of reality. 

I’ve got a different algorithm that I go through although alas it seems rather less directed than Feynman’s.  1) think very hard, 2) write down the solution, 3) write down the problem.  Like … it’s nice when you realize that what you’ve been thinking about actually applies to things the rest of the world cares about, however the process of getting there involves thoughts that are difficult justify.  

What I’ve been thinking about ‘recently’ feels like a *thing*, but unfortunately I’m pretty deep into the first step of Inman’s problem solving algorithm.  This might simply be me rediscovering something that everyone else is already aware of or it might be me noticing a bunch of suspicious looking things that in reality do not have any actual relation to one another.  Hard to tell, but I want to try to express some of this.

This probably started with type theory.  Which then lead to category theory.  It turns out you can use F Algebras [3] to convert a recursive data structure into a non recursive data structure.  And I guess this is just the category theory description of work from domain theory [4] (check out lecture 2 about recursively defined programs).  Self referential mathematical objects caused a lot of problems in set theory, so there was some interest in eliminating these problems from recursive definitions in lambda calculus in order to ensure there was no formal issues that would prevent it from being used as a model for denotational semantics.  And while I’m on the domain theory topic, I’ll go ahead and mention that domain theory’s creator Dana Scott also came up with a rather neat observation:   computable functions are just scott continuous functions [13].  

Okay, so far we’ve seen two weird things.  The first is that there is some sort of relationship between recursive data and non recursive data.  The second is that we can treat computability as a mathematical object.  Let’s move on.

While poking around in category theory and f algebras, of course I couldn’t help notice discussions regarding co recursion [2].  Specifically, a HN user, Pitarou, mentioned something about co recursion and transforms [1].  The gist of the comment is that there is asserted, but not proved, a path from a recursive algorithm to a stream algorithm via co recursion and then from the stream algorithm to an iterative algorithm via deforestation techniques and tail call optimization.  

Much like the first observation concerning a transform from recursive data structures to non recursive data structures, we now see a transform from recursive algorithms to iterative algorithms.  Granted we don’t see the same rigor as we do from domain theory’s explorations, however just the idea is the important bit.  Keep moving.

Derandomization [5] is a technique for converting a randomized algorithm into a non randomized algorithm with possibly some slow down.  There are a bunch of techniques for accomplishing this, but I don’t think there’s any proof yet that all randomized algorithms can be derandomized (although I believe it is thought that this is the case).  This of course sounds vaguely similar to Pitarou’s recursive algorithm to iterative algorithm transform.  A thing that sounds about right but no proof that it’s possible for all inhabitants of its space.

Relatedly (because complexity theory) is the subtitle to Scott Aaronson’s blog [6].  “Quantum computers … can be simulated classically with exponential slowdown.”  While I’m aware that blog subtitles aren’t proofs, I have heard this before from several independent sources (and Scott Aaronson is a much better complexity theorist than I will probably ever be), so let’s call this one “proved” for the time being.

Interesting, we’ve got a relationship between recursive data and non recursive data and a relationship between classical computers and quantum computers both of which stand on firm theoretical grounding.  Additionally, we’ve got derandomization that sounds good but is unproved and a recursion to iterative process that also sounds good but is unproven.  All of that seems vaguely like the same sorts of things are going on (in some sense of those words).

Along comes HN user tel who starts a pretty interesting blog series concerning mutable algorithms in an immutable context [7].  Meanwhile HN user jerf clarifies and indicates a transform from mutable algorithm to immutable algorithm [8] really ought to exist.  I’m not sure that I buy jerf’s argument, but that’s just because I haven’t been able to get the whole algorithm into my head yet.  I think there’s some ambiguity with the description that will be resolved if I actually step through it manually with an example, however I’m not sure what problem I’m actually trying to solve so I haven’t convinced myself to go through that exercise yet.  Either way I’m already dealing with several other transforms that don’t have “totality” proofs yet, so I’m perfectly happy placing this (rather incredible even if only partial) transform in a pending state mentally for now.  

The point is that this yet another computer science thingy transform from one side of the fence to the other.  Normally the discourse is concerning iterative vs recursive or immutable vs mutable or classical vs quantum.  However, again and again I’m bumping into arguments that these things are really the same thing or perhaps one of them is just the ‘bigger’ version of the other.  Okay, only two more things to work though and I think I’m done.

I’ve long thought that lisp macros [10] and Λ abstraction in system f [11] feel really similar.  I’m not exactly sure what I’m suggesting here, but it feels sort of like it belongs in the same (or a similar) category as the rest of the transforms here.

Finally, I wrote kind of a weird monadic parser [9].  I’ve also used a similar method to convert a data structure that had a lot of implicit properties into a data structure that made those properties explicit.  The idea being that maybe there’s some sort of relationship between unstructured data and structured data that can be represented by monads, and maybe that sort of thing is similar to some of the other ideas I’ve been encountering.

Short story long.  It looks a lot like *something* is going on between things that are normally thought of as opposite sides of the spectrum.  

Thursday, January 9, 2014

Good Software

For some time now, I've been working on the theory that people are different.  Go ahead pause to consider if you really want to continue reading.  

Seriously?  People are different ... and you've been working on this theory "for some time"?  Maybe if I left now I would have enough time to finish that sudoku.

Well, there's a little bit more to it than just that.  So let me set the scene a bit and I think you'll see that there's something here to consider.  Also there could be some horrifying consequences that will render the Software Engineering Industry asunder.  Destroying the lives of hard working men and women whose only crime was doing their jobs.  Meanwhile these same consequences will facilitate the first megalomaniac sociopath who realizes the implications and has the means and ambition to act on them to rebuild the Software Engineering Industry in their own image.  You know of what I speak.  A barren wasteland where Software Engineers form primitive tribes to survive.  And tire armor.  Yeah!  Tire armor for everybody!  TIRE ARMOR FOREVER!!!

Okay, maybe not that.  But it might explain *some* of the reasons why everyone yells at each other so much about programming languages.  And … it could provide someone who's really clever (and owns a software engineering company) to build more efficient teams and ensure better code base quality over time.

The situation today

Is that software kind of sucks.  The best in the world are able to just barely create software that does what we want without emailing our social security number straight identity thieves.  

Right now your best bet for getting software that works is to find a small group of highly motivated smart people who get along (but who also secretly hate each other, just a little bit) and put them into a room under the guidance of "that guy".  You know.  That guy who pesters all of your stake holders for every minor detail of what they want until the stake holders decide that they were better off doing it manually.  That guy who refuses to sign off on the release until you get 200% code coverage, user studies successfully completed by a homeless man from a different country who doesn't speak the language the application displays and who is completely illiterate, and finally all of the integration tests are successfully run by a blind monkey.  No not a code monkey like a real monkey.

Then you give that team complete autonomy and a budget that is two hundred percent of what the estimates tell you, and they still fail to deliver anything useful half of the time.

All of this assumes that you don't need any security in your application.  If it needs to be secure, then you need the same thing with some minor changes.  Your highly motivated team of smart people also need to have PhDs.  Like each one needs to have multiple PhDs.  Also they each need no less than five (5) and no more than eight (8) graduate students all of whom were child prodigies.  Finally, they each need to have been doing computer security work for at least 30 years (and it wouldn't hurt if they were spies in the cold war).

You still need "that guy", but he also needs some upgrades.  And unfortunately, you'll never find him.  He has to find you.  Just assemble your team and put out a press release that you're interested in maybe creating a secure application some day.  Pay the team to do research or something.  Perhaps they can create prototypes of what the final secure application could be like.  Just don't get jittery and use one of the prototypes because it's "good enough".  Because it's not good enough.  

Eventually, that guy will show up.  You'll probably find him in your house one day after work.  He will ask you questions and you will answer them.  Don't worry about getting them correct because you cannot get them correct.  He is only interested in how you fail.  

Once "that guy" finds you and he leads your team to construct your secure application, do not forget the final step.  It is vital that you have a plan for when some bored Russian undergrad proves that the Chinese have been putting hardware viruses in the sand that is used to create the computer chips that your application runs on and *that* allows the NSA to trigger the backdoor that they hid in number theory, which devastates the entire security model of your application causing it to immediately email your social security number to every identity thief on the planet.

The right way to write software

Is almost definitely a myth.  Which is actually kind of the point that I wanted to start with.  People are different.  This has consequences for how they create software.  Unfortunately, the completely true picture I drew above concerning the state of software development today gives a very big incentive to charlatans who will try to sell you "the right way to write software".  Try not to be too hard on them, there's a large chance they don't realize that they are charlatans.  Their methods might even work … for them.  And maybe their methods even work for people sufficiently like them.  But their methods don't work for everyone.  Also if you try to cheat by only employing people who are all sufficiently similar, you'll get destroyed when they encounter a problem that they can't get their heads wrapped around, but which literally any other developer on the planet could solve in twenty minutes (but not if they have to code like *that*).

At one point in time I think I really wanted to find "the one way" to program.  It was going to be the right way to program, it would let me work faster, it would eliminate bugs, and I could teach it to everyone.  Then one day when I was knee deep in type theory, trying to decide if domain theory or category theory should be the next topic that I venture into, when I happened to consider the economic side of perfect software.  Can a company actually bill it's clients enough or can an internal software division procure a sufficient budget to pay for the software engineer who is also a computer science category theorist?  The only reason that I spend time trying to decide whether I like dependent types or general algebraic data types with polymorphic kinds better is because I'm lonely and weird.  Normal people have lives.

And then there's the evidence.  I kept on bumping into problems that I couldn't solve without much frustration, but normal software engineers seem to be able to tackle without any problems.  Can trying to figure out Sequent Calculus in your free time ruin you as a software engineer?  Well, no that doesn't make sense either because I also kept bumping into problems that normal software engineers found incomprehensible, but that I could solve trivially.  A suspicious pattern that suggests that there's no best way of thinking that allows you to solve all problems.  Let's take a look at an example.

TDD vs Parametric Polymorphism (ie type theory stuff)

There are two claims that have been floating around on the internet.  They sound very similar to each other, but you wouldn't want to assert that they are the same.  At least don't if you want to stay out of trouble.  The first is the TDD claim:  "I write my tests first and that allows me to write correct code."  The second is the Hindley-Milner type inference claim:  "When my program type checks, then I know it's correct."

To me, both of these claims sound like magical thinking.  I do this thing, which has a totally intrinsic and completely unexplained and unexplored ability to manifest "correct" software regardless of the constraints of physical reality, and my software just somehow works completely correct.  The first time.  Every time.  

I don't buy that TDD is *the* way to write software because I have rarely found anyone who can actually explain to me what it is or why it works.  The people who do give me an actionable definition have always given me a different actionable definition than the previous person who gave me an actionable definition.  I suppose I wouldn't be opposed to trying TDD in practice, however I would first need to actually understand what it is I'm suppose to be doing.  Write the test first and then correct software is emitted isn't a well defined algorithm.

I don't buy that Hindley-Milner type inference is *the* way to write software because I know about dependent types.  And universal quantification, and polymorphic kinds, and general algebraic data types.  Even assuming you upgrade your Parametric Polymorphism, popularized in languages that use Hindley-Milner like inference such as ML or Haskell, to a dependently typed system and then go on to prove everything you can think of about every last function, then you still have to worry about an impedance mismatch between the problem you're solving and the actual code.  A perfectly proven algorithm doesn't protect you against misidentifying the problem you were trying to solve.

However!  Both types of people write software that works!  It isn't perfect, but it does mostly solve the problem and allows you to get on with your life.

So my theory at least for now is that people are different.  They don't think the same, they don't work the same, and they don't write software the same.  And that's just something we're going to have to deal with moving forward in the Software Engineering Industry.  I'm not sure exactly what this means that we should do, but I do think this means that we can't settle on "the one way" to write software.  At least if we want to be able to write good software.