Another Word For It Patrick Durusau on Topic Maps and Semantic Diversity

December 2, 2018

Programming Language Foundations in Agda [Hackers Fear Not!]

Filed under: Agda,Computer Science,Cybersecurity,Hacking,Programming,Proof Theory — Patrick Durusau @ 11:47 am

Programming Language Foundations in Agda by Philip Wadler and Wen Kokke.

From the preface:

The most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that a certain kind of formal structure may be read in two ways: either as a proposition in logic or as a type in computing. Further, a related structure may be read as either the proof of the proposition or as a programme of the corresponding type. Further still, simplification of proofs corresponds to evaluation of programs.

Accordingly, the title of this book also has two readings. It may be parsed as “(Programming Language) Foundations in Agda” or “Programming (Language Foundations) in Agda” — the specifications we will write in the proof assistant Agda both describe programming languages and are themselves programmes.

The book is aimed at students in the last year of an undergraduate honours programme or the first year of a master or doctorate degree. It aims to teach the fundamentals of operational semantics of programming languages, with simply-typed lambda calculus as the central example. The textbook is written as a literate script in Agda. The hope is that using a proof assistant will make the development more concrete and accessible to students, and give them rapid feedback to find and correct misapprehensions.

The book is broken into two parts. The first part, Logical Foundations, develops the needed formalisms. The second part, Programming Language Foundations, introduces basic methods of operational semantics.

Hackers should attend closely to Wadler and Kokke’s text to improve their own tools. The advantages of type-dependent programming are recited by Andrew Hynes in Why you should care about dependently typed programming and I won’t repeat them here.

Hynes also reassures hackers (perhaps not his intent) that a wave of type-dependent programming is not on the near horizon saying:

So we’ve got these types that act as self-documenting proofs that functionality works, add clarity, add confidence our code works as well as runs. And, more than that, they make sense. Why didn’t we have these before? The short answer is, they’re a new concept, they’re not in every language, a large amount of people don’t know they exist or that this is even possible. Also, there are those I mentioned earlier, who hear about its use in research and dismiss it as purely for that purpose (let’s not forget that people write papers about languages like C and [Idealized] Algol, too). The fact I felt the need to write this article extolling their virtues should be proof enough of that.

Like object orientation and other ideas before it, it may take a while before this idea seeps down into being taught at universities and seen as standard. Functional programming has only just entered this space. The main stop-gap right now is this knowledge, and it’s the same reason you can’t snap your fingers together and have a bunch of Java devs who have never seen Haskell before writing perfect Haskell day one. Dependently typed programming is still a new concept, but that doesn’t mean you need to wait. Things we take for granted were new once, too.

I’m not arguing in favour of everybody in the world switching to a dependently typed language and doing everything possible dependently typed, that would be silly, and it encourages misuse. I am arguing in favour of, whenever possible (e.g. if you’re already using Haskell or similar) perhaps thinking whether dependent types suit what you’re writing. Chances are, there’s probably something they do suit very well indeed. They’re a truly fantastic tool and I’d argue that they will get better as time goes on due to way architecture will evolve. I think we’ll be seeing a lot more of them in the future. (emphasis in original)

Vulnerabilities have been, are and will continue to be etched into silicon. Vulnerabilities exist in decades of code and in the code written to secure it. Silicon and code that will still be running as type-dependent programming slowly seeps into the mainstream.

Hackers should benefit from and not fear type-dependent programming!

March 9, 2015

Programs and Proofs: Mechanizing Mathematics with Dependent Types

Filed under: Coq,Functional Programming,Proof Theory,Software Engineering,Types — Patrick Durusau @ 3:49 pm

Programs and Proofs: Mechanizing Mathematics with Dependent Types by Ilya Sergey.

From the post:

coq-logo

The picture “Le coq mécanisé” is courtesy of Lilia Anisimova

These lecture notes are the result of the author’s personal experience of learning how to structure formal reasoning using the Coq proof assistant and employ Coq in large-scale research projects. The present manuscript offers a brief and practically-oriented introduction to the basic concepts of mechanized reasoning and interactive theorem proving.

The primary audience of the manuscript are the readers with expertise in software development and programming and knowledge of discrete mathematic disciplines on the level of an undergraduate university program. The high-level goal of the course is, therefore, to demonstrate how much the rigorous mathematical reasoning and development of robust and intellectually manageable programs have in common, and how understanding of common programming language concepts provides a solid background for building mathematical abstractions and proving theorems formally. The low-level goal of this course is to provide an overview of the Coq proof assistant, taken in its both incarnations: as an expressive functional programming language with dependent types and as a proof assistant providing support for mechanized interactive theorem proving.

By aiming these two goals, this manuscript is, thus, intended to provide a demonstration how the concepts familiar from the mainstream programming languages and serving as parts of good programming practices can provide illuminating insights about the nature of reasoning in Coq’s logical foundations and make it possible to reduce the burden of mechanical theorem proving. These insights will eventually give the reader a freedom to focus solely on the essential part of the formal development instead of fighting with the proof assistant in futile attempts to encode the “obvious” mathematical intuition.

One approach to change the current “it works, let’s ship” software development model. Users prefer software that works but in these security conscious times, having software that works and is to some degree secure, is even better.

Looking forward to software with a warranty as a major disruption of the software industry. Major vendors are organized around there being no warranty/liability for software failures. A startup, organized to account for warranty/liability, would be a powerful opponent.

Proof techniques are one way to enable the offering limited warranties for software products.

I first saw this in a tweet by Comp Sci Fact.

December 27, 2014

Software Foundations

Filed under: Coq,Functional Programming,Programming,Proof Theory,Software Engineering,Types — Patrick Durusau @ 4:49 pm

Software Foundations by Benjamin Pierce and others.

From the preface:

This electronic book is a course on Software Foundations, the mathematical underpinnings of reliable software. Topics include basic concepts of logic, computer-assisted theorem proving and the Coq proof assistant, functional programming, operational semantics, Hoare logic, and static type systems. The exposition is intended for a broad range of readers, from advanced undergraduates to PhD students and researchers. No specific background in logic or programming languages is assumed, though a degree of mathematical maturity will be helpful.

One novelty of the course is that it is one hundred per cent formalized and machine-checked: the entire text is literally a script for Coq. It is intended to be read alongside an interactive session with Coq. All the details in the text are fully formalized in Coq, and the exercises are designed to be worked using Coq.

The files are organized into a sequence of core chapters, covering about one semester’s worth of material and organized into a coherent linear narrative, plus a number of “appendices” covering additional topics. All the core chapters are suitable for both graduate and upper-level undergraduate students.

This looks like a real treat!

Imagine security in a world where buggy software (by error and design) wasn’t patched by more buggy software (by error and design) and protected by security software, which is also buggy (by error and design). Would that change the complexion of current security issues?

I first saw this in a tweet by onepaperperday.

PS: Sony got hacked, again. Rumor is that this latest Sony hack was an extra credit exercise for a 6th grade programming class.

November 24, 2014

Jean Yang on An Axiomatic Basis for Computer Programming

Filed under: Logic,Programming,Proof Theory — Patrick Durusau @ 2:56 pm

Jean Yang on An Axiomatic Basis for Computer Programming (slide deck)

From the description:

Our lives now run on software. Bugs are becoming not just annoyances for software developers, but sources of potentially catastrophic failures. A careless programmer mistake could leak our social security numbers or crash our cars. While testing provides some assurance, it is difficult to test all possibilities in complex systems–and practically impossible in concurrent systems. For the critical systems in our lives, we should demand mathematical guarantees that the software behaves the way the programmer expected.

A single paper influenced much of the work towards providing these mathematical guarantees. C.A.R. Hoare’s seminal 1969 paper “An Axiomatic Basis for Computer Programming” introduces a method of reasoning about program correctness now known as Hoare logic. In this paper, Hoare provides a technique that 1) allows programmers to express program properties and 2) allows these properties to be automatically checked. These ideas have influenced decades of research in automated reasoning about software correctness.

In this talk, I will describe the main ideas in Hoare logic, as well as the impact of these ideas. I will talk about my personal experience using Hoare logic to verify memory guarantees in an operating system. I will also discuss takeaway lessons for working programmers.

The slides are impressive enough! I will be updating this post to include a pointer to the video when posted.

How important is correctness of merging in topic maps?

If you are the unfortunate individual whose personal information includes an incorrectly merged detail describing you as a terrorist, correctness of merging may be very important, at least to you.

The same would be true for information systems containing arrest warrants, bad credit information, incorrect job histories, education records, and banking records, just to mention a few.

What guarantees can you provide clients concerning merging of data in your topic maps?

Or is that the client and/or victim’s problem?

August 11, 2014

Archive of Formal Proofs

Filed under: Formal Methods,GPU,Proof Theory — Patrick Durusau @ 1:47 pm

Archive of Formal Proofs

From the webpage:

The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle. It is organized in the way of a scientific journal, is indexed by dblp and has an ISSN: 2150-914x. Submissions are refereed. The preferred citation style is available [here].

It may not be tomorrow but if I don’t capture this site today, I will need to find it in the near future!

Just skimming I did see an entry of interest to the GPU crowd: Syntax and semantics of a GPU kernel programming language by John Wickerson.

Abstract:

This document accompanies the article “The Design and Implementation of a Verification Technique for GPU Kernels” by Adam Betts, Nathan Chong, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer, Paul Thomson and John Wickerson. It formalises all of the definitions provided in Sections 3 and 4 of the article.

I first saw this in a tweet by Computer Science.

February 5, 2014

Proof Theory Foundations

Filed under: CS Lectures,Proof Theory — Patrick Durusau @ 1:02 pm

Frank Pfenning’s lectures from the Oregon Programming Languages School 2012, University of Oregon.

Lecture 1

Lecture 2

Lecture 3

Lecture 4

Unlike the astronomer in Rasselas (Chapter 41), it is insufficient in serious CS discussions to “know” you are correct. 😉

Taught along with Category Theory Foundations and Type Theory Foundations.

Powered by WordPress