An intriguing title, referring to one of those subjects I hadn't quite got round to investigating yet - still on my to-do list was to listen to an interview with Miles Sabin talking about, amongst other things, dependent types.

Although Miles was at the conference on the first day, he wasn't around on the second, so I missed my chance to talk to him. However, there was always the panel discussion, so I made do ;-) with addressing a question to Martin Odersky on the matter (22:20 mins into the video).

Here's what he had to say, with my own, possibly wrong-end-of-the-stick, embellishments:

- There's an interesting area between Haskell and maths, that's populated by programming languages [featuring dependent types] such as Agda, and theorem provers such as Coq.
- According to the Curry-Howard Isomorphism,
- there's a strong correspondence between types and properties [of programs] (so we can encode the properties of programs in types);
- [By properties of programs is meant things like the property of associativity of the concatenation operator of a list.]
- if a type is a property [of a program], then the [existence of that working] program [involving that type] is a proof of that property.
- Certain theorems in maths (e.g. Four-colour theorem) can only be proved (practically) by writing a program [in a language like Agda, expressing the theorem as dependent types].
- Applications of such proofs in computing are currently somewhat specialised/limited:
- proof of correctness wrt attacks on cryptographic systems.
- proof of correctness of whole programs, using theorem provers such as Z3 to do the constraints solving, is currently limited to programs in the 10s of lines.
- Scaling of proof of whole-program correctness to much larger programs, or the obviation of unit tests, is unlikely to happen any time soon.
- We are constrained by the need to reconcile that which it is possible to do with types, with that which humans can comprehend.
- Having type systems which are easy to use is the more pressing challenge.

look at

ReplyDeletehttp://www.ertos.nicta.com.au/research/l4.verified/approach.pml

http://www.seas.upenn.edu/~sweirich/talks/flops2012.pdf

So, details of an application, involving Haskell, to operating systems (to make them more secure), and the slides for a talk on 'Dependently-Typed Programming in GHC'.

DeleteLooks interesting (particularly the slide on 'Why Dependent Types?') - thanks.

thank you for giving such valuable information.one of the recommanded site.we appriciate more details

ReplyDeleteHadoop,spark, and scala training

Scala training in hyderabafd

Hadoop training in hyderabad

Magnificent blog I visit this blog it's extremely wonderful. Interestingly, in this blog content composed plainly and reasonable. The substance of data is useful.

ReplyDeleteOracle Fusion HCM Online Training

Oracle Fusion SCM Online Training

Oracle Fusion Financials Online Training

Big Data and Hadoop Training In Hyderabad

oracle fusion financials classroom training

Workday HCM Online Training

Oracle Fusion HCM Classroom Training

Workday HCM Online Training

oracle cpq online training / Oracle CPQ Class Room Training

Oracle Taleo Online Training