Software consulting focused on quality.
"Problems are solved through thinking, not writing code."
What is correct code?
Both of the following functions break a sentence into multiple lines, given maximum width - however:
This signature can be implemented in an infinite amount of ways.
This one - about four, where three aren't using all the parameters.
Correct code means guaranteed properties.
Guaranteed properties means no surprises.
No surprises means no hidden time, money or complexity costs!
Does your software exhibit any of the following traits?
In addition, do you:
These are predictable and -sadly- common outcomes of applying any methodology as an ideology.
Our brand of tweaks we call CorrectlyCoded is compatible to any methodology you chose: clean code, TDD, extreme programming, and we guarantee emphasization of all of its useful traits.
Practically speaking, we can bring out useful traits even out of pure chaos!
Correctly Coded Highway
All software is incepted through a vision of a better process and an automation idea. These are often abstract, unstructured concepts, so it is vital that they get translated into more structured form.
Ergo, all software development is translation of ideas, where correctly structured ideas produce correct software.
We address these issues through replicable, teachable process that converts Your vision into entities that exhibit strong matehmatical structure. We dig deep into the processes regularly applied in science and academia, and we distill them into business and production practices.
CorrectlyCoded highway has four lanes that all go in the same direction:
Category theory modelling
UML is a great communication language, but unfortunately a poor structural modelling language. This trait is a consequence of its simple design decision: it doesn't impose structural constraints on modelling. In order to summon correct architecture with it, one has to tap into experience and intuition - which is, again, translation of historical data into current problem, and it is not always applicable.
Category theory is a math discipline used -among other things- to formalize other mathematical structures, such as sets and rings.
Category theory embodies the essence of composition , which is a vital property when designing large and abstract solutions through composition of smaller, well-defined and pre-existing solutions.
Solving problems by breaking them into smaller problems is the definition of how we do software development today, so category theory is a very useful tool to adopt.
Ergo, you are not constrainted by access to (expensive) experience any more; you can rely on a strong tool with guaranteed properties instead.
Composable, modular architecture
Vision translated into properly structured model exhibits properties which guarantee reusability.
Software that works by composing well-defined pieces strongly decreases maintenance costs because of one very important property: you can cut glue that composes modules and analyze each part of the system in isolation.
This property is called purity.
Properly constructed model also guarantees at the very least one mathematically strong way of composing its components, such as functions, functors, monads - or even dependent types.
These are useful, because they offer plenty of ways to compose modules in different ways and retain their useful properties!
Finally, all these details bring one very powerful advantage: you don't have to answer questions, to which you don't have well-defined answers, such as: how will this software evolve through time.
Every business which relies on software, needs to be able to adapt said software quickly and efficiently.
Adopting purity as a core concept, allows you to do exactly that!
Most modern software production today relies on automated testing to witness its correctness.
Curry-Howard isomorphism is a powerful tool that takes this notion and pushes is few steps further: it allows software to ensure its correctness by encoding business logic directly into type system of the host language.
This means that software that doesn't follow business rules - can't be built into an executable binary!
Take a moment to ponder on this.
Software that guarantees its correctness before it is even executed!
At CorrectlyCoded we use range of techniques that Curry Howard isomorphism inspired, that in turn ensure our software has highest degree of compile-time safety. Among many others, we rely on algebraic data, dependent typing and explicit side-effects.
Our software allows for very precise business logic definitions, and catches errors before the code is even built.
It is precisely because of this, that we guarantee our clients lifetime maintenance and support! We know that support for software written this way is trivial.
Testing software is inevitable part of witnessing its correctness, and when coupled with all previous lanes of CorrectlyCoded Highway, it reliably proves that software behaves during execution exactly as we envisioned it would during construction.
One way to elevate testing is to abandon discrete, almost arithmetic way of writing tests and adopt algebraic approach:
Adopting this technique ensures that not only you catch runtime invariant errors that you potentialy didn't test for, but also forces you to think about execution context in terms of contracts it should hold.
These techniques, coupled together and applied in parallel during all cycles of software development, ensure that the product is of highest possible quality.
This, in turn, ensures that your development and subsequent recurrent costs are the lowest they can be.
Software that is formally correct doesn't break
Correct software welcomes additions and changes, as they are forced to surrender to same qualitative properties.
Correct software costs less to develop and to maintain.
How can we help?
Give us a call and lets talk! There are numerous ways to take advantage of our skills, and we can both find the way that suits you the best.
Most of collaboration can be summed down into variation of the following:
Software development as a service
Because we develop software to be future-proof, and we're strictly following the business philosophy of 'put your money where your mouth is' - all software developed by us has a lifetime guarantee of maintenance and support!
Our people will happily join your existing teams, asses your improvements plan, adapt to your style and process and help you reach your goals quicker. Additionally, they'll spot little potentials for process optimization as they go, and introduce our standards of quality and correctness to it.
John is unforgettable because of his authenticity. He brings a true creative dynamic in Dev team, always aiming to the best...
Anne-Marie Mallet, HR Lead @ Tempo
...his ability to work with complex problems and come up with elegant solutions is what impressed me the most with his work. He has demonstrated strong analysis and design skills as well as very strong programming abilities in many languages...
Eric Chailler, CTO @ FXInnovation
...by continuously expanding his knowledge not only in computer science, but also in other domains, he inspires his team to do the same. Combined with his rich and diverse experience, John is able to handle any technical challenges coming his way...
Thomas Rohee, Data scientist @ Logibec
.. have never worked with a programmer so passionate about programming... an amazing team player and all around good person...
Tyson McCann, Sr. Product manager @ SkipTheDishes
...an extremely talented programmer with a focus on doing things right the first time...
Craig Morisson, Design Department Manager @ Blizzard Entertainment
...an asset to our organization during his tenure with the studio... has excellent written and verbal communication skills, is extremely organized, can work independently and is able to follow through to ensure that the job gets done...
Miguel Caron, Head of Baltic Studios | General Manager @ Gamesys Estonia
...a constant driving force for any team and is always promoting open communication and a positive atmosphere...
Daniel Dahl, Art director | Lead artist | Founder @ Jellyfish Games
... has passion for technologies, algorithms and coding practices. Combined with his professionalism and cooperativeness, it makes him a must have member of any project.
Ping Ng, Mobile system developer @ Giant leap technologies, AS
Ramblings and rants about gritty details (a.k.a. blog), coming right here in a bit!
CorrectlyCoded uses Happstack
john - [at] - correctlycoded [dot] com