> it's misleading to assume that ... types always have to be based on some underlying ideas form functional programming.
One of FP's more annoying achievements is somehow convincing people that it's the only way to make programs more verifiable or more "mathematical". Imperative, stateful computation can be (and is) just as mathematical (whatever that means) and just as verifiable as pure-FP (it must be constrained in some ways, but not as extreme as requiring complete referential-transparency).
It's good to learn about applying types to process calculi. I wasn't aware of that work at all.
Imperative, stateful computation [...] is [...] as [...] verifiable as pure-FP
Exactly. When you verify your programs using some kind of program logic you realise that you have to keep track of all relevant data anyway.
The condescension towards languages like C/C++ and Java that some FP extremists have shown is probably one of the reasons for the rift between working programmers and PL theory. Fortunately, things are much better now, with most new languages (e.g. Scala, Rust, Clojure) bridging both worlds.
applying types to process calculi. I wasn't aware of that work at all.
Maybe "A Gentle Introduction to
Multiparty Asynchronous Session Types" http://goo.gl/FeVLv3 could be an introduction?
>The condescension towards languages like C/C++ and Java that some FP extremists have shown is probably one of the reasons for the rift between working programmers and PL theory. Fortunately, things are much better now, with most new languages (e.g. Scala, Rust, Clojure) bridging both worlds.
Look, if you want to build a whole language around Hoare logic, go ahead. We just think it's ugly.
You don't need to build a "whole language" around any kind of logic for it to be sufficiently verifiable. Types are useful, but it's not necessarily an all-or-nothing question. There are non-type-based verification tools (symbolic execution and deduction), and tests complete the picture. A language that doesn't let you write a program unless you yourself have worked hard to prove to the compiler that it's correct may be more trouble than it's worth. Verification does not necessarily have to be a part of compilation, and it does not necessarily require the proof to be spelled out in code.
I agree that it is good separate programming and verification. Otherwise the programmer is forced by the compiler to
worry about correctness and termination from Day 1.
Moreover, Cury-Howard based approaches really work only for a
restricted form of programming: pure and total functions.
I'm not sure I can follow you here. What is ugly, Hoare logic? What does it mean to "build a whole language around Hoare logic"? What in your opinion are the alternatives to Hoare-style program logics that are general-purpose enough to work for arbitrary programming languages?
One of FP's more annoying achievements is somehow convincing people that it's the only way to make programs more verifiable or more "mathematical". Imperative, stateful computation can be (and is) just as mathematical (whatever that means) and just as verifiable as pure-FP (it must be constrained in some ways, but not as extreme as requiring complete referential-transparency).
It's good to learn about applying types to process calculi. I wasn't aware of that work at all.