mrb

My basic point is that currently, configuration management code manifests as a giant, unverifiable pile of mud. The languages we use lack types and are weak at making non-runtime assertions. With the modicum of sanity that a proper module system and types can bring to the table, we would be considerably better off.

mrb

"This picture of evolving software suggests the mildly paradoxical concept of software reliability. Normally one says that a program is either correct or incorrect; either it works or it does not work. But like any complex organism, a large software system is always in a transitional situation where most things work but a few things do not, and where fewer things work immediately after an extensive change. As an analogy, we say that hardware is reliable if it does not break too often or too extensively in spite of wear. With software, we say that an evolving system is reliable if it does not break too often or too extensively in spite of change. Software reliability, in this sense, is always a major concern in the construction of large systems, maybe even the main concern. This is where type systems come in. Types provide a way of controlling evolution, by partially verifying programs at each stage. Since typechecking is mechanical, one can guarantee, for a well designed language, that certain classes of er

mrb

Q: Who are you, and what do you do?

mrb, I sell software.

Q: What hardware do you use?

Huh? My laptop.

Q: And what software?

mrb

require 'rtc'

class Post
  rtc_annotated

  typesig('@id: String')
  attr_accessor :id
  
  typesig('@title: String')
  attr_accessor :title

mrb

module Main
 
import Effect.State
 
data BTree a = Leaf
             | Node (BTree a) a (BTree a)
 
instance Show a => Show (BTree a) where
  show Leaf = "[]"
  show (Node l x r) = "[" ++ show l ++ " "

mrb

module Main
 
import Prelude.Algebra
 
instance Semigroup Nat where
  (<+>) = (*)
 
instance VerifiedSemigroup Nat where
  semigroupOpIsAssociative = multAssociative

mrb

h.idr:12:27:
When elaborating right hand side of Prelude.Algebra.Nat instance of Prelude.Algebra.VerifiedMonoid, method monoidNeutralIsNeutralL:
Can't unify
        (right : Nat) -> fromInteger 1 * right = right
with
        (l : Nat) -> mult l neutral = l

Specifically:
        Can't unify
                plus v0 0

mrb

module Main

import Prelude.Algebra
 
instance Semigroup Nat where
  (<+>) = (*)
 
instance VerifiedSemigroup Nat where
  semigroupOpIsAssociative = multAssociative

mrb

6:16 AM <haasn> Are there any immediate examples that come to mind when talking about “unsolved questions/problems related to dependent typing”?
6:16 AM <haasn> Like, are there any big questions left to answer by the forefront of DT research?
6:19 AM <christiansen> haasn: can HoTT compute?
6:19 AM <christiansen> can we make usable programming languages that also work for programming in the large?
6:19 AM <christiansen> what idioms work well for programming with dependent types?
6:20 AM <christiansen> how do we deal with totality and codata in a way that isn't a pain in the ass?
6:23 AM <ziman> how to compose dependent programs?
6:24 AM <christiansen> how to avoid writing 117 kinds of lists to make the indices do what we want?
6:24 AM <christiansen> some of these have starts
6:24 AM <christiansen> oh, separate compilation and good performance

mrb

"A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute." - Pierce, TAPL