The Alma project, or how first-order logic can help us in imperative programming