Poohbist Technology provides high quality software, specializing in provable programming languages. Festina lente. Bruta fulmina. Make haste slowly. Thunderbolts strike blindly.

Downloads

NummSquared 2006a0 is a new well-founded functional foundation for logic, mathematics and computer science.

Short paper: "NummSquared: a New Foundation for Formal Methods"

Samuel Howse's completed PhD thesis: "NummSquared 2006a0 Explained"

Slides on NummSquared Coercion

Slides on NummSquared

Logician's Toolkit integrates various logical tools, including Coq, with MSBuild, the build system used by Microsoft Visual Studio .NET 2005.

Back to "Contents"

About the Developer, Sam Howse (born 1980, died 2008)

During October 2006, Dr. Samuel (Sam) Howse, PhD Computer Science and MA Economics, completed a new foundation for logic, mathematics and computer science. Part of this groundbreaking work was the specification of a functional programming language called NummSquared.

At the invitation of L'École Polytechnique, France's foremost university of engineering and applied sciences, Sam traveled to Paris to present his research. There, in November 2006, he entered into discussions with colleagues including Gilles Dowek and Hugo Herbelin on the future of functional programming languages. Drs. Dowek and Herbelin are prominent in the Coq and OCaml development communities.

A few weeks later, in January 2007, Sam was diagnosed with cholangiocarcinoma (cancer of the bile ducts and liver), of which he would die in January 2008. He was then 27 years old.

To build a more robust foundation for computer science was a lifelong ambition for Sam. From the age of seven, he taught himself about the design of computer hardware and software, initially using BASIC on a Tandy CoCo.

One of the uses Sam immediately found for computers was in educating other people. He taught his three-year-old brother, Joe, to read and type using Sierra adventure games.

At 15, Sam began formally studying computer science in continuing education and university courses. At 19, he became an instructor and introduced Java to the cirricula of DalTech Continuing Technical Education and Dalhousie University.

Outside academia, Sam's employment had included a team role in developing software for naval design. This experience, in part, shaped his thinking on the importance of software correctness in applications that have high human or economic costs of errors.

Healthcare was another field of applications that concerned Sam. He had seen family members suffer from diagnostic errors and failures of information management. He volunteered in a children's hospital, the IWK Health Centre, for five years until his own illness. He studied healthcare economics as part of his Master's degree.

Ultimately, Sam felt that people deserve better than today's mainstream programming languages and practices that lack proof of correctness. This concern was his fundamental motivation in furthering the evolution of fuctional programming languages.

A human error delayed Sam's diagnosis by two years and thus greatly shortened his lifespan. Such a failure would not have happened on Sam's watch—and a better system would have caught it sooner.

Correctness, so often, is a matter of life.

Back to "Contents"

Sam's Acknowledgements

For software engineering, computer support, digital media, data mining, research and customized training, ask Nummist Computer Consultants.

We work closely with our friends at Nummist Media and Eucatastrophic Creations.

Our fearless founder, formally Rt. Hon. Leo L. Lion (informally, Plumpy or Mr. P):

Rt. Hon. Leo L. Lion

For two decades, Mr. P, the Aged Aged Man, was a patient but determined advocate of formal methods.

Back to "Contents"

Poohbist Technology