u/sankeldin r/haskell • Recommends
Using Agda to design and refactor C++ programs (video)
0:00 / 0:00
#agda#denotationalsemantics#c++templates
David Sankel: The Intellectual Ascent to Agda
CppNow
39K subscribers • 42 videos on Hallway • Conference channel
- Recommended by 2 people: 2 in engineering communities.
- Presented by David Sankel
Advanced. Deep dive for people who know the field.
9.4K views13 years ago2 recommendations
Programming languagesSoftware designC++Functional programmingLanguage design and type systems
David Sankel explains how to apply denotational semantics and denotative design to derive robust C++ programs using the Agda language.
When one thinks of math and computer science what often comes to mind are asymptotic analysis and mind-bending algorithms for physical simulations. A branch that usually slips through cracks is denotational semantics, the math of syntax and meaning. Denotative design, denotational semantics put into practice, is a top-down design methodology that produces simple, composable, and incredibly powerful libraries that are in an entirely different league from what is commonly available. It is especially suited to C++ which has a sufficiently powerful templating engine. In this session, we will learn how to apply denotative design by deriving C++ programs from domain-specific mathematical entities using the syntax of Agda, a pure functional and dependently-typed language. --- *--* ---Why it's here
2 people recommend thisWhat people say. Recommended for developers interested in using type theory and denotational semantics to design and refactor C++ libraries.
Moments people linked to
u/gelisamin r/haskell • Mentions
On “Once you've seen the beautiful, you don't want to go back to the ugly”
So the good news is that there are techniques I've learned in Haskell which transfer very well to other languages. One bad news, of course, is that there are also techniques which don't transfer, and that's frustrating. But the bad news I want to talk about is that even those techniques which do transfer well, you might not get to use them either :(
Here's a story.
After rescuing a buggy project by applying FP principles to a Java app, I felt like knowing Haskell had given me super powers. But then I moved on to a more conservative team, on a C++ project. C++ is really not a bad language for putting functional programming idioms to good use. And so when the team was looking for an alte…
u/pipocaQuemadain r/haskell • Mentions
On “I've got functional curse. I lost my ability to write in C++. I have to ship C++. What do I do?”
David Sankel does a lot of functional programming in C++.
He gave a talk at boostcon, The Intellectual Ascent to Agda. There's also a pdf he wrote, Modern Functional Programming in C++.
Take a look at boost::variant, and also boost::lambda
u/ertesxin r/haskell • Mentions
On “Heartbleed aftermath: should Haskell web frameworks allow using a pure Haskell SSL library instead of OpenSSL?”
I understand your point, but there are only very few architectures that can run asymmetric cryptography code but can't run the Haskell RTS. For those other (and probably better) options are available. There is at least one guy who generates his C++ from Agda.
For the achitectures where Haskell is available we shouldn't interface with C code. We have the option to write a high quality pure Haskell TLS library, and Vincent is already delivering it. Better help him improve that one rather than going back to the legacy we want to get rid of in the first place.