Posts tagged "programming language"
1985 Dijkstra interview October 10, 2007
Continuations, continued. October 22, 2007
sigfpe: Monads, Kleisli Arrows, Comonads and other Rambling Thoughts November 6, 2007
Re: Template Insanity November 12, 2007
Arrows? December 12, 2007
Coq and The Maybe Monad December 17, 2007
Some [More] Notes on the Abstraction Penalty for IA86 C++ Compilers February 25, 2008
Quote o' the day March 21, 2008
Carving wire November 20, 2008
Scala problem #1 January 10, 2009
API design and granfalloons July 9, 2009
Whatever happened to symbolic links? November 26, 2009
Einstein's problem December 24, 2009
Phantom Types in Java June 19, 2010
Phantom Types in Java, Revisted July 5, 2010
Subclassing and Java Generics July 31, 2010
Monads and regular expressions August 8, 2010
Variations on the theme of monadic regular expressions: Abstraction September 6, 2010
Variations on the theme of monadic regular expressions: Records September 13, 2010
Variations on the theme of monadic regular expressions: Back references September 14, 2010
"(How to write a (Lisp) interpreter (in C++) (or make Peter Norvig cry, whichever comes first))" October 11, 2010
Quote o' the Week: It’s [Not] Faster Because It’s C October 12, 2010
Link o' the day: Meditations on Bluish Coder and inadequacy October 27, 2010
Subclassing and Java Generics, revisited November 3, 2010
Knights, knaves, and Program Construction November 11, 2010
Finger Trees November 25, 2010
More Phantom Types in Java December 9, 2010
Measured Finger Trees December 11, 2010
Equational programming December 25, 2010
Tony Morris on static types May 9, 2011
When Domain Specific Languages Attack! June 4, 2011
Some Lisp suggestions June 17, 2011
Snakes! On a Yeti! July 4, 2011
Some notes on A Tour of Go October 5, 2011
Link o' the Day: Everyones first quantum program October 7, 2011
Quote o' the Day: Appel fanbois October 18, 2011
Systems programming November 1, 2011
Link o' the day: Donald Knuth, Tony Hoare, and goto November 4, 2011
Link o' the day: Roslyn and eval for C# November 17, 2011
Quote o' the day: Coda Hale on the value of communities November 30, 2011
Mad science, abstract data types, and objects December 12, 2011
Quote o' the day: Criticism December 24, 2011
Link o' the day: Java and memory February 9, 2012
Link o' the day: Matt Might on parsing with derivatives March 31, 2012
Parsing with derivatives: introduction April 16, 2012
Parsing with derivatives: recursion April 28, 2012
Quote o' the day: OMG! Something from Steve Yegge! May 18, 2012
Parsing with derivatives: compaction May 22, 2012
JavaScript: The Good Parts June 26, 2012
On the definition of object oriented programming July 14, 2012
Quote o' the day: Slightly over the top September 12, 2012
Quote o' the day: The award for best function name goes to... December 14, 2012
Brian Harvey on Scheme vs. Python January 30, 2013
Exploring Rust February 17, 2013
Rust Iterators February 21, 2013
Creating a Letterpress cheating program in Rust February 25, 2013
Link o' the day: The Deep Insights of Alan Kay March 8, 2013
Creating a Letterpress cheating program in Rust, v2 March 9, 2013
Creating a Letterpress cheating program in Rust: Traits March 26, 2013
Letterpress cheating in Rust: Parallelism April 7, 2013
Letterpress cheating in Rust: Parallelism part 2 April 16, 2013
Operator overloading in Rust April 26, 2013
mmap and the Rust Foreign Function Interface June 12, 2013
Letterpress cheating in Rust 0.7 July 6, 2013
Rust 0.8: External iterators October 5, 2013
Letterpress cheating in Rust 0.8 October 6, 2013
A faster hashmap in Rust October 12, 2013
Quote o' the day: All you really need to know about PHP December 17, 2013
Letterpress cheating in Nimrod? December 23, 2013
Flex- and BisonModules updated (sort of) December 28, 2013
Link o' the day: static vs. dynamic typing battles January 14, 2014
Quote o' the day: Mmmm, pudding January 23, 2014
Automatic memory management: reference counting February 12, 2014
Automatic memory management: hybrid reference counting March 1, 2014
Letterpress cheating in Rust 0.11.0, part 1 July 19, 2014
Type-safe C? August 8, 2014
Letterpress cheating in Rust 0.11.0, part 2 August 9, 2014
One stupid shell scripting trick everyone should know April 11, 2015
Another Rust spot: delegation January 21, 2016
Letterpress cheating in Rust 1.6: How long has it been?!? January 27, 2016
Quicksort February 14, 2016
Push-parsing and Pony July 2, 2016
Hey, let’s write a quick parser! A simple one, for the simple version of hoc from The Unix Programming Environment. The chapter on hoc is used to demonstrate the use of the yacc parser; it’s a dandy example to play with parsing.
I haven’t hand written a parser in a long time, so that’s what I want to do now. But there is a bit of a catch: it reads from stdin in Pony. And the interface for that is:
interface StdinNotify
"""
Notification for data arriving via stdin.
"""
fun ref apply(data: Array[U8] iso) =>
"""
Called when data is available on stdin.
"""
None
fun ref dispose() =>
"""
Called when no more data will arrive on stdin.
"""
NoneA deep dive into regular expression derivatives for lexical analysis August 15, 2016
Although I (embarrassingly) never completed the project, I have written before on derivative-based parsing,1 the work of Matt Might and others. The recent appearance of On the Complexity and Performance of Parsing with Derivatives and a certain immediate interest in parsing re-awakened my curiosity about the subject. (And no, it’s not because Might’s derivative-parsing tool is called Derp (but as an added bonus, the pure recognizer version is “herp” (and the accompanying regular expression package is “rerp”)).2) In this particular post, I would like to demonstrate why I think the technique is cool, by demonstrating that derivative-based regular expressions are cool.
To that end, I’ll start with regular expression matching, then go on to the conversion to a deterministic finite automaton and finally discuss the minor extras needed to build a lexical analyzer, similar to lex or flex (but better).
Read more…The pain of learning Rust January 19, 2017
I recently saw several posts from ESR discussing his attempts to learn Rust, for use in rewriting NTPsec: “Rust vs. Go” and “Rust severely disappoints me”, as well as “Rust and the limits of swarm design”. These posts gave me the incentive to write down some thoughts I have on the difficulty of approaching Rust. In pariticular, I have noticed are some commonalities among those who have initial difficulties with Rust’s ownership model.
Read more…Applied Formal Logic: Brute Force String Search June 19, 2017
Need is there, but tools are not.
– zzz95
Let’s play with Frama-C.
Read more…Applied Formal Logic: The bug in Quick Search June 23, 2017
In my last post, I presented a brief introduction to Frama-C and to the process of verifying properties about a very simple C function, a brute force string search. This time around, I intended to do roughly the same thing, using a slightly more complicated function, a faster string searching algorithm. Unfortunately, in doing so, I found a bug in the algorithm. Admittedly, the bug is rather minor and should not affect the actual behavior of an implementation in practice, but still, it is doing something it shouldn’t ought to be doing.
The string searching algorithm I am looking at this time is Quick Search, so named by Daniel M. Sunday in 1990 because it “is a simple, fast, practical algorithm [and] because it can be both coded and debugged quickly” (“A Very Fast Substring Search Algorithm” [PDF]. It is my personal favorite string search because it is, indeed, simple, fast, and practical. Let me quickly show why.
Read more…Applied Formal Logic: Correctness of Quick Search July 16, 2017
When last I left, I had verified that the implementation of Quick Search was safe: the modified algorithm didn’t access memory it shouldn’t, it didn’t have numeric overflows, and it didn’t modify anything outside of its own implementation. And, using Frama-C, the process hadn’t hardly been torturous or even particularly unpleasant at all. The most important tasks were describing the requirements for calling the two functions. Those requirements are…detailed…but nothing more than what an experienced C programmer would have in mind while writing or calling the functions. A final set of shiny set of annotations ensured that the loops and the variable modifications needed by them behaved themselves.
But I hadn’t done anything about proving that the function actually did what it claimed it was supposed to do. It’s not hard to understand (one of the reasons I like Quick Search), but the ANSI/ISO C Specification Language is unfamiliar and I didn’t know how to express what went on, where. Fortunately, Yannick Moy, a software engineer at AdaCore, came to my assistance with an excellent introduction to doing the same thing with SPARK, and Loïc Correnson, one of the creators of Frama-C, popped in with some excellent suggestions (and very flattering comments).
So now, for your software verification pleasure, here is my essay at proving the correctness of Quick Search. It pretty much follows the same pattern as Yannick’s, but I did come up with a slightly different postcondition for make_bad_shift.
Applied Formal Logic: Verifying Quicksort August 9, 2017
Have you ever tried to solve a problem, gotten stuck, backed off, tried again, changed approaches, failed, and then suddenly, with some approach that you’d already abandoned, solved the problem as sweetly as Penelope Doglington begging for part of your sandwich? I’ve had one of those weeks, and now I honestly don’t know what the problem was. Everything seems to be all better now.
So, here it is: my proof of Quicksort. The proof, which is mine, is mine. And therefore, my proof, which belongs to me, is as follows.
Read more…On Complete Gibberish August 15, 2017
Or, Programming language syntax that I don’t like
We interrupt our regularly-scheduled nonsense (Wait! Did someone make up a schedule? Nobody told me! – mcguire) for a brief screed on programming language syntax.
Read more…Software Foundations, Volume 1: Logical Foundations December 8, 2017
There is a certain amount of celebration going on at Maniagnosis’ underground lair at the moment. (Underground lair? There’s nothing underground or lair-ish about this place. It’s not even spectacularly office-like. –Ed) I have (Insert lame drum-roll here.) completed all of the exercises in Software Foundations, Vol. 1: Logical Foundations by Benjamin Pierce, et al. (Very much al.)
(Cue fireworks!) Pop!
Read more…