Home » forums » LtU Forum

'Mindless coding': following proof steps makes algorithms easy

Mindless Coding, uses Coq to emit Ocaml:

Fully-specified dependently typed structures (avltree and rbtree) and their functions (find, insert, delmin and delete) not only produce fully verified results - they also reduce the task of function implementation to a stepwise refinement of intermediate steps (proof subgoals) that are constrained to the point where the programmer (prover) is freed from consideration of the overall algorithm involved during each step. In many cases, the steps are fully automatable. In others, the information provided by the subgoal's context, along with a "rough idea" of what the algorithm being implemented should do, is usually sufficient for the programmer to make progress to the next subgoal.

Perhaps the best illustration of this "mindless" point is the implementation of the complex rebalancing functions for Red-Black trees, which are widely viewed as difficult to do correctly. These were implemented using this "mindless-coding" technique without relying on any outside explanatory material or implementations.

'Mindless' if you are smart enough to be able to do incremental steps in proof-making :-)

By raould at 2014-07-14 21:08 | LtU Forum | previous forum topic | next forum topic | other blogs | 4448 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Same old story

Autocoders (aka assembly languages) were designed to make programming unncessary and obsolete. They did — for the definition of "programming" that involves nothing but pure machine coding. But formal thinking remains formal thinking no matter how high-level the tools are, and not everyone can do it.

By johnwcowan at Tue, 2014-07-15 02:20 | login or register to post comments

Even worse: it can't be

Even worse: it can't be applied to much of the crud non-algorithmic code that we write; we are plumbers more often than mathematicians. I haven't balanced a red-black tree in a very long time, and I can't really empathize with this.

By Sean McDirmid at Tue, 2014-07-15 03:00 | login or register to post comments

Does it feel like plumbing because you're using the wrong tools?

A UX designer can do the UI for a business application in HTML/CSS and you can write the code in Javascript, or have a nodejs or Python service to do the work for a multi-user application. The UX designer can build the whole frontend, the backend is executing a command protocol that does the actual work. Backend tools like Django (Python) can create the backend for a database service automatically from the SQL schema, so most business applications are all about the schema, then automating the processes.

You could consider tools that create code from schemas the process driven equivalent of the above. Further being able to derive code from constraints, for example specifying process constraints like only one package can be selected at a time, all people must be employees, and have the code generated seems useful. Red/black trees seem an abstract example, but could well emerge naturally from industrial process constraints like a mail sorting machine. All business processes are defined by constraints of some kind.

By Keean Schupke at Tue, 2014-07-15 05:02 | login or register to post comments

and, tools in the semantic sense

if we had good specs and spec languages for UI/UX/etc. then we could possibly be doing more of the TDD/Mindless approaches to implementing the code. i feel like we just generally don't have anything close enough to math or logic for them. which is lame/sad. hope to quickly be proven wrong and pointed to logics for UI/UX :-)

By raould at Tue, 2014-07-15 21:11 | login or register to post comments

Well, we do have design

Well, we do have design languages, but you can't really formalize human behavior.

By Sean McDirmid at Tue, 2014-07-15 23:30 | login or register to post comments