[ukj]

Software Engineers: Parse, don't validate.

Mathematicians: Parsing is validation

https://gallais.github.io/pdf/draft_sigbovik21.pdf

[Drup]

To everyone in this subthread: sigbovik is a conference published every 1st of April.

This paper is an April's fool joke. I didn't think people could take that one seriously. I guess it's a good April's fool then. :)

[ukj]

The conference is indeed a spoof, but in so far as what Mathematicians call a "proof" - the paper contains one. Agda is a proof assistant in the spirit of the Calculus of Constructions ( https://en.wikipedia.org/wiki/Calculus_of_constructions ).

So is the joke on Computer Scientists or Mathematicians? You decide ;)

Beware of bugs in the above code; I have only proved it correct, not tried it --Donald Knuth

[Drup]

Sigbovik's jokes are of the kind where the premise is completely bonkers. The rest of the development is made with the utmost rigor to highlight said bonkersitude, Reductio ad absurdum.

[ukj]

Yeah, but that is precisely how inductive types work.

"Bonkers" premises. Iterate, iterate, iterate. "Bonkers" conclusions. GIGO.

And yet the result is reified, exists and speaks for itself. So what is so "absurd" and "bonkers" about a result that is right before your eyes?

https://en.wikipedia.org/wiki/Reification_(computer_science)

[rualca]

The wide adoption of Flask as Python's backend development framework of choice makes it quite clear that software developers have a hard time picking up April fool's jokes.

[411111111111111]

Or how great April fool's ideas can actually be if they turn out to be real

[cjfd]

Software engineers like efficiently running software. Mathematicians like beautiful definitions. Scientists like non-trivial discoveries.

This paper.... uh.... what exactly is it good for?

I suppose it could be kind of nice as some kind of undergraduate paper writing project kind of thing but it looks too professional for that.... I am kind of at a loss why this was written. Maybe it is some strange kind of satire....

[squiddev]

It's written for sigbovik 2021 [1][2], which is very much a joke conference. Other papers this year were "Lowestcase and Uppestcase letters: Advances in Derp Learning" and "On the dire importance of mru caches for human survival (against Skynet)".

[1]: http://www.sigbovik.org/ [2]: http://www.sigbovik.org/2021/proceedings.pdf

[m3koval]

SIGBOVIK is a parody of computer science conferences. It's a running joke hosted on April Fools Day every year at CMU - and apparently a quite convincing one. ;-)

Source: I attended SIGBOVIK a few times in grad school.

[ukj]

This paper is good for parsing/validating your source code (from the view-point of your compiler/interpreter).

Code is data after all.

[pwdisswordfish8]

The point being, the converse of ‘parsing is validation’ is not true.

[ukj]

Then you have some formally inexpressible/impredicative notion of "validation" in mind. For posterity (lifting from the depths of the threads):

General case: Validating random data as input into some program.

Particular case: Validating random source code (data) as input into some compiler (program).

Do compilers parse or validate?

> "the converse of ‘parsing is validation’ is not true."

If that were the case then you should be able to give an example of a compiler validating random source code (data) but not parsing it.

What determines the validity of random input is precisely a compiler's ability to parse it.

[nsajko]

I think that you actually agree with the comment you responded to, it's just that you misinterpreted what it was trying to say.

[ukj]

I certainly don’t disagree (that doesn’t mean I agree).

The purpose of the conversation is to arrive at mutually acceptable interpretation.

[ukj]

The word "is" implies an isomorphism.

If you see it differently you are implicitly assuming a non-formalist perspective on what "validation" means. Tell us about it.

[pwdisswordfish8]

‘A square is a rectangle’ means squares are isomorphic to rectangles?

[ukj]

You are tripping up over polymorphism. "Is" means many things - which meaning you infer is precisely parsing!

"A square is a rectangle" means "A square is a TYPE of rectangle" (at least, that is what I am parsing it as).

"Parsing is Validation" means Parsing is isomorphic to Validation.

How do I know? Because that is how I want you to parse it.

[pwdisswordfish8]

> 'When I use a word,' Humpty Dumpty said in rather a scornful tone, 'it means just what I choose it to mean — neither more nor less.'

[ukj]

+∞

parse verb. resolve (a sentence) into its component parts and describe their syntactic roles.

In computer science what we do is precisely syntax analysis. Determining the meaning of operators.

Mathematicians have the exact same problem with respect to the equality operator.

https://ncatlab.org/nlab/show/equality#DifferentKinds

[jhgb]

> "A square is a rectangle" means "A square is a TYPE of rectangle" (at least, that is what I am parsing it as).

In that case your former statement that 'The word "is" implies an isomorphism' seems to be wrong.

[ukj]

It may be wrong in your model/interpretation of my words, but it's not wrong in my interpretation of my words.

[thereare5lights]

> The word "is" implies an isomorphism.

Are you talking about a bijective mapping or are you saying it's a synonym for identical?

Because the former doesn't make any sense here and the latter is not true.

Red is a color does not imply that all colors are red.

[ukj]

I am talking about the polymorphic use of the verb "is" during the process of formalization.

"Red is a color" can be formalized as "Red is a type of color" or "Red is member of set Colors".

You can't formalize "Color is red" because it doesn't mean anything.

When I say "Parsing is validation" I am using the verb "is" to mean an isomorphism.

[thereare5lights]

Judging by all the other disagreeing comments, your in some sort of idiosyncratic context that only you understand.

Good luck with that.

[codetrotter]

The word “is” is also often used informally to mean “is a kind of”.

[ukj]

"A kind of" is precisely its formal use from the PoV of a type theorist.

Two things are the same type of thing if they share all of their extensional properties.

That is what it means for two things to be identical/equal.

[codetrotter]

But what I am saying is that parsing is a kind of validation. But all validation is not parsing.

For example let's say that I have written an HTTP API that accepts application/x-www-form-urlencoded data to one of its endpoints. Let's say `POST /users`, and this is where the client-side application posts data to.

Now I can implement this in many ways. I can for example define

    pub struct Person {
        name: String,
        phone_number: String,
    }

But how I populate this struct can determine whether I am actually parsing or not, even if most of the code aside from that is the same.

And of course I could go further and define types for the name and the phone number but in this case lets say that I have decided that strings are the proper representation in this case.

If the fields of my structs were directly accessible

    pub struct Person {
        pub name: String,
        pub phone_number: String,
    }

And in my HTTP API endpoint for `POST /users` I do the following:

    // ...
    
    let name = post_data.name;
    let phone_number = post_data.phone_number;

    let norwegian_phone_number_format = Regex::new(r"^(\+47|0047)?\d{8}$").unwrap();

    // ...

And I didn't bother to write out the rest of the code here for this example but you get the gist.

The point is that here I am doing some rudimentary validation on the phone number, requiring it to be in Norwegian format. But I am enforcing this in the implementation of the handler for the HTTP API endpoint, rather than in the data type itself.

Whereas if I was instead doing

    pub struct Person {
        name: String,
        phone_number: String,
    }

    impl Person {
        pub fn try_new (name: String, phone_number: String) -> std::result::Result<Self, PersonDataError> {
            // ...

            let norwegian_phone_number_format = Regex::new(r"^(\+47|0047)?\d{8}$").unwrap();

            // ...
        }
    }

Now I've moved the validation into an associated function of the type itself, and I've made the fields of the struct unaccessible from the outside.

And in this manner, even though my validation is still rudimentary, and a type purist might find the type insufficiently constrained, I have indeed in my own book gone from just validation to actual parsing. Because I have made it so that the construction of the type enforces the constraints on the data.

[ukj]

You are over-complicating this into obscurity.

General case: Validating random data as input into some program.

Particular case: Validating random source code (data) as input into some compiler (program).

Do compilers parse or validate?

"parsing is validation, but validation is not parsing" if that were true then you should be able to give an example of a compiler doing some sort of validation on the random source code (data) that is not parsing.

The very thing which determines the validity of random source code is the compiler's ability to parse it.