This is the same for Haskell where it's also convenient to develop in the repl (ghci).

There's the repl, and then there's nREPL. I do like ghci, but I can't execute arbitrary chunks of Haskell directly from Vim.

This isn't a function of ghci or Haskell, that's an editor feature. If you want that kind of functionality than emacs is probably your best bet.

Though you can send arbitrary code blocks from vim using vim-slime.

[1] https://github.com/jpalardy/vim-slime

Though you can't execute arbitrary blocks of text in Haskell. Almost everything non-trivial will require adding a slew of "let"s, not all statements are available in GHCi, and state gets wiped on every reload.

When I first began developing Haskell, coming from Clojure, these issues drove me crazy. Nowadays I don't miss them too much and doubt that they're really such good features to begin with...

But it's decidedly false to claim that GHCi is as flexible as Clojure's repl. Nowadays, Clojure's repl would make me anxious. It reminds me a bit of people doing live code edits on a production server. You can't ever be quite sure what you get.

What is it with the obsession with regular expressions? They are useful things, sure, but I just use them in connection with grep or if I search for strings and normally they are pretty basic, e.g.

$ grep -r -n --color "foo*bar" src

If I want to validate input data with the machine I just use a parser.

Regexes are an elegant and very powerful way to validate data in scripts in a concise (and if they aren't abused) easy to read fashion. There are almost infinite number of examples, but let's say I want to verify that a field is a 64 Bit hexadecimal MAC address

   $mac =~ ^[A-Fa-f0-9]{16}$

Gets the job done. How else, but a regular expression so concisely?

And, when you say, "If I want to validate input data with the machine I just use a parser." - that's pretty much what a regex engine is - a sophisticated parser, and the regular expression is the "commands" that you feed to it to parse the input text.

Here is another one I just did tonight - I wanted to match IPv4 addresses, but didn't want to validate anything with a leading 0 (specifies octal format, which 99.9999% of the time is not what people want), but I do want to accept a leading 0 if it's the only value (I.E. 3.0.2.1, 0.0.0.0, etc...)

regex_ipv4='^((25[0-5]|2[0-4][0-9]|1[0-9]{2}|[1-9][0-9]|[0-9])\.){3}(25[0-5]|2[0-4][0-9]|1[0-9]{2}|[1-9][0-9]|[0-9])$'

Gets the job done.

How else would you do it?

You can then build up a library of these, and use them on other projects.

Maybe something like this:

  def is_ipv4_addr(s):
     try:
        octets = s.split('.')
        assert len(octets) == 4
        for o in octets:
            assert 0 <= int(o.lstrip(0) or '0') < 256
     except:
        return False
     return True

It is longer; on the other hand, it is easier to read and more importantly easier to verify correctness.

Would:

  1. 12 .13. 14
  089.23.45.67

Both match that? (Your general point is made though - RegExes look fine to the person that just crafted them, but are opaque to the casual observer)

I think you forgot to verify that an octet doesn't have leading zeros (unless its value actually is zero).

I didn't forget: the (o.lstrip(0) or '0') expression does that.

Actually, that should be o.lstrip('0')...

Wrong.

  >>> is_ipv4_addr("01.0.0.0")
  True

It should reject that (i.e. return False) because the first octet contains a leading zero. But you're just stripping the zero away, ignoring its existence. For no effect, because converting with int() already ignores them for you.

Your code is also ok with bizarre inputs like "0..." :-)

Regexes really do have their strengths -- they compactly express a state machine, and you can always break the expression into parts which'll show exactly what the state machine will accept. They could also be much more readable if people bothered to break them into parts instead of typing it out all inside a long string that becomes really difficult to parse visually. There are other notations to improve readability, for example rx in emacs: http://www.emacswiki.org/emacs/rx

A seemingly simple regex can be implemented in imperative code and it might look clean and pretty until you get the logic exactly right and amend it to handle all the corner cases that are not obvious at first sight. For comparison I did the exercise in old-fashioned C (and the indentation got messed up along the way, sigh).

https://pastebin.mozilla.org/3171656

A state machine would be more appropriate in my opinion.

You're right. My mistake.

I like automata and I think regexes are good for some things, but I definitely agree about the crappy syntax. When working in CL, I loved Edi Weitz' CLPPCRE package which allowed you to specify regexes using either the traditional broken string form or an s-exp syntax. Much cleaner.

> How else would you do it?

Taking your question generally, I was curious to see what it might look like as a parser, since I find that regex a little hard to read. Here's an implementation with Haskell's parsec:

https://gist.github.com/mjhoy/6751909

Ok then maybe it's just a matter of taste. I like the parser approach more:

import Text.ParserCombinators.ReadP -- or the parser lib of your choice

import Data.Char

...

macP = count 16 (satisfy isHexDigit)

I don't think your example does what you think it does, match fo followed by o zero or more times, followed by bar.

when you do understand regex, you'll be amazed at the myriad of things you can do with it.

You are absolutely right, I forgot the '.'.

You are talking about halvm I think - is it still in use or is it a dead project? The github project page does not seem to have seen commits for a while, but maybe it just ... works.

And can you please point me to the talk?

Here's the talk: http://www.haskellcast.com/episode/002-don-stewart-on-real-w...

thanks!

Just wanted to say, kudos! I think it is essential for a language to have a good C interface otherwise it will be insulated. However some more example would be nice. Furthermore I think you mean "infix" in your documentation and not "inline".

... and one should always remap ESC. For me this was a big improvement (from an ergonomic viewpoint). My suggestion:

imap jf <ESC>

Maybe I should take a look at awk/sed but I never found its language orthogonal. For simple scripts I mostly use Python or Haskell via something like

ghc -e 'interact ((++"\n") . show . length . lines)' < file

EDIT:

I know that it's the same like "wc -l" but using that approach I can solve also problems that may not be well suited for awk/sed. Or maybe I just have to see some convincing one-liners.

There is also a fun part in the documentation of xorg.conf, just do

$ man xorg.conf

and search for "nobody"

;)

If you are interested in chilled thoughtful gaming and have a faible for SciFi ala Star-Trek and Co. you MUST try FTL. It is one of the best games I have ever played and I do not know another game that is similar. It is easy to learn and hard to master and although it is Single-Player it has an immense replay potential.

My biggest improvement was about finding out about .inputrc and configuring the Bash to use VIM-keybindings which is pretty handy if you are used to the editor. Also the following mapping from ESC to pressing jf via

imap jf <ESC>

was very nice as I find it much more ergonomic. And to use it in Bash I have

set editing-mode vi set keymap vi

$if mode=vi set keymap vi-insert "jf": vi-movement-mode $endif

set show-all-if-ambiguous on

I have my Bash set to vi keybindings, but I had no idea it was possible to remap them. Now I can finally stop hitting escape in Bash too. Thank you so much!

Yeah it is great if you can use similar commands across applications. Btw. there is also a nice history inside VIM (implemented as a separate buffer) that can be accessed using q: so you can scroll through the history with jfkl. E.g. I use that for accessing files: If you are working on a project you will probably edit similar files. If you use one "programming" vim sessions where you always edit files via :tabe you will find all the recent edited files in your history and using q:/ you can search for them pretty fast. So over time you have automatically a working environment adapted to your current project.

How does this work, if the kernel is supposed to be TM-complete?

1) The halting problem only states that you cannot create a program that can decide whether any given program will finish. It is possible for special cases, though.

2) They didn't automatically verify the kernel. Coq is a proof assistant.

The halting problem is also decidable for finite memory machine, like our real ones, so ...

Yes, but our memory is so big and our machines can have so many states that the problem is still intractable in the general case.

But still very much solvable in the specific domains of real world applications.

You know what. I think I agree with you. I would actually go as far as to posit that most common applications don't require a Turing-Complete environment to run. If you could strip away the trouble spots and limit yourself to what you really need you can get a lot back in terms of software checking and assurance.

That's awesome. Thanks for sharing. It's nice to know that people a lot smarter than me are thinking about this already :).

I may be wrong, but AFAICT, the kernel in question is basically an API layer between the real browser and the OS.

The point of the exercise is to prove that something like a file read cannot be invoked with bad files and cannot cause buffer overflows etc..

That doesn't require turing completeness.