Dependent types

So, why are you not using dependent types yet? Do you like your programs randomly crashing?

>>40
That none of what you just described happens at compile time.

>>41
>>17 happens at runtime.

>>42
Yes, >>17 crashes at runtime instead of warning you at compile time, which is my point.

>>43
How >>17 would behave at compile time with dependent types? C++ version with setters/getters on protected boxed value would work fine at runtime.

>>44
It would complain that the type of the array is something like Vect n Int while the head function requires a value of type Vect (n + 1) Int

C++ version with setters/getters on protected boxed value would work fine at runtime

The issue is that the compiler will not warn you if you forget or mis-implement said getters/setters. See >>24

>>45

while the head function requires a value of type Vect (n + 1) Int

In that case dependent types are safer.
Its likely possible within the class to add static_assert or exotic set of constexprs to fail template instantiation, but your argument is that the programmer can also fuck up the static_assert/constexpr's too. There is however a modern alternative to this, C++ concepts:

C++ concepts can be enabled in gcc with -fconcepts and is probably the closest thing to implementing dependent type
https://gcc.gnu.org/onlinedocs/gcc/C_002b_002b-Concepts.html

>>46
Concepts seems like some form of proof checker or something, which is somewhat close to dependent types indeed - seems similar to what F* uses.
But I might have just misunderstood what concepts are about, this seems like a new thing.

>>47
Its just advanced syntax sugar for static_assert on constexpr's which takes template parameters or other constexpr's.
See https://en.cppreference.com/w/cpp/language/static_assert

https://www.boost.org/doc/libs/1_48_0/libs/concept_check/using_concept_check.htm
Boost had this before current_year C++ standards

The future C++20 standard has concepts(aka constraints), but its still not adopted by all compilers, support is poor except GCC.
https://en.cppreference.com/w/cpp/language/constraints

#define STATIC_ASSERT( compile_time_expr ) typedef char __STATIC_ASSERT__[( compile_time_expr )?1:-1];

>>50 The Virgin constraint
>>51 the Chad impossible array

>>45
Would that also mean scanf equivalent function needs to implement handling dependent types as output?
How would this look in idris?

>>53

Would that also mean scanf equivalent function needs to implement handling dependent types as output?

No

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
template<typename T,size_t size> class contain {private: T arr[size];
public:
T operator [](size_t i) const{
if(!(i<size)){puts("Requested Index out of range. Aborting");exit(2);}
return arr[i];};
T& operator[](size_t i) {
if(!(i<size)){puts("Input Index out of range. Aborting");exit(1);}
return arr[i];};};

int main(){
contain<int,50> A;
int i;
int rts=scanf("%d", &i);
A[i] = 100;
printf("%d", A[i]); return rts;} Edited on 15/10/2018 04:53.

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
template<typename T,int size> class contain {private:	T arr[size];
template<typename T,size_t size> class contain {private:	T arr[size];
public: 
T operator [](size_t i) const{
if(!(i<size)){puts("Requested Index out of range. Aborting");exit(2);}
return arr[i];};
T& operator[](size_t i) {
if(!(i<size)){puts("Input Index out of range. Aborting");exit(1);}
return arr[i];};};

int main(){
contain<int,50> A;
int i;
int rts=scanf("%d", &i);
 A[i] = 100;
 printf("%d", A[i]); return rts;}

>>54
In that case what the program will do on invalid input?

>>54
Lets reiterate:
1.Scanf-equivalent outputs integers
2. ...
3.Dependent type accept only restricted subset of integers.
What is happening at #2

>>55
Hi FrozenANUS

>>55
Someone did not read the thread, huh? See >>45

>>56
Whatever the programmer chose.

>>57
2. The programmer verifies that the input is correct and in such a case passes it to the function.

>>59
Why should I have to verify the input? That's the computer's job.

>>60
...
What?

>>61

The programmer verifies that the input is correct

Why doesn't the computer do it?

>>62
Could you explain clearly what you mean by that please?

all input should be verified server-side

client-side input validation is not secure

>>63
I assume he wants for dependent types(proof checker) to verify input too. Removing the manual check("The programmer verifies that the input is correct") from the program.

>>65
lmao @ you thinking ``muh dependent types'' will solve ALL input validation issues ever

it's not that simple, buddy

>>66
What makes you think that?

>>67
if it was so simple, we'd have done it by now

why would corporations who stand to lose a lot by getting hacked avoid something that would make them hack-proof? because it's not a magic bullet like you say it is, that's why

>>68

if it was so simple, we'd have done it by now

But we have.

why would corporations who stand to lose a lot by getting hacked avoid something that would make them hack-proof?

Because it is cheaper to hire Indians for pennies who have no idea about dependent types than hire people with some CS background. Why do you think that crap like Windows and Java are so popular?

There’s no way you can encode all the logic to sanitize input in just types.

B-b-but you can write code that output types!

But I can also directly write that code without types as a middleman.

>>70

There’s no way you can encode all the logic to sanitize input in just types.

What makes you think that? Haven't you heard of Curry–Howard isomorphism?

But I can also directly write that code without types as a middleman.

Code that you can't prove that is correct, sure. This is why most programs nowadays are unstable and full of vulnerabilities.

>>69
this guy thinks he has security 100% figured out

kek dude, you don't even know what you don't know

>>72
Please do feel free to correct me. Can you?

>>73
https://www.exploit-db.com/
https://www.cvedetails.com/
you remind me of the ``infinite compression'' thread
you think complex problems have super simple solutions and that they're already solved, which is not the case

>>74

https://www.exploit-db.com/
https://www.cvedetails.com/

All I see are bugs in software written in C and Java, neither of which have dependent types.

which is not the case

What makes you think that in this specific case?

>>75
cybercrime causes billions of dollars in damages every year, and you, posting on a low-traffic textboard, claim to know the solution

if you really knew a solution, you should try to profit off it

or, more likely, you're just talking out of your ass, and security is a little more complicated than mere dependent types, because you don't know shit about infosec

will dependent types stop someone from clicking on a link? will it stop SQL injection? will it stop word docs/maldocs/macros? will it stop JS embedded in PDFS? will it stop ransomware? will it stop cryptojacking? will it stop keylogging? will it stop RATs? will it stop XML external entity attacks? will it stop reflected XSS? DOM XSS? CSRF? remote file inclusion? local file inclusion? billion laughs? UDP reflection? UDP amplification? NTP reflection? default passwords? overflows? numeric underflows? slowloris resource exhaustion? predictable session tokens? predictable resource location? sybil attacks? hash cracking? social engineering? covert channels? data exfiltration? privilege escalation? reverse shells? steganography? file descriptor attacks? vlan hopping? arp spoofing? shatter attacks? SSRF attacks? cache poisoning? DNS hijacking? DHT poisoning? CTS flooding? smurf attacks? fraggle attacks? format string vulnerabilities? array indexing errors? mismatched array new/delete? stack overrun? unused values? file handle leaks? OSINT/opsec issues? predictable TOTP? dns exfiltration? exfil via x.509 metadata fields? content-type header injection? WMI hijacking? UEFI rootkits? network resource leaks? debug features left on in production? compiler backdoors? ephemeral netcat backdoors? hardware backdoors? side channel analysis? rowhammer bit-flipping? van eck phreaking? null pointer dereferencing? uninitialized/improperly initialized memory? lack of proper ASLR? checksum collisions? port knocking? clickjacking? DNS sinkholing? remote code execution? VM escapes? missing lower bounds? iterator invalidation of mutable data structures leading to undefined behavior? data inferrence? misconfiguration? directory enumeration? unhandled return codes? hooking? return pointers to local variables? invalid use of negative values? passing large parameters by value? underallocations of dynamic data? nop sleds? heap spraying? heap pointer replacement? JIT spraying? race conditions?

there are hundreds and hundreds of other attack vectors I know about that I could post but it's late and I'm drinking and need to fall asleep soon

>>76
Most of these have nothing to do with programming languages themselves. Some of them in fact are physics related (van eck phreaking) or people related (social engineering). This thread is about dependent types solving bugs in software.

privilege escalation?
overflows? numeric underflows?
null pointer dereferencing? uninitialized/improperly initialized memory?
format string vulnerabilities? array indexing errors? mismatched array new/delete? stack overrun? unused values?
remote code execution?
iterator invalidation of mutable data structures leading to undefined behavior?
unhandled return codes?
return pointers to local variables? invalid use of negative values?
underallocations of dynamic data?

Yes, dependent types protect against these.

file handle leaks?
network resource leaks?
race conditions?

Pretty sure that you need linear types for these.

There are probably some that I missed.

>>1

So, why are you not using dependent types yet? Do you like your programs randomly crashing?

What if NPCs are incapable of writing safe code by design? They lack the level of abstract thought required to imagine the code being exploited. They just write code as requested by design and wonder why it randomly crashes and allows exploits.

>>78
I once contributed to an open source project (game) where the leader was incapable of considering his ideas being exploited against his vision.
It was pain.

Average software quality will be greatly improved and even programmers who write 99% safe code will benefit. Even C++ concepts-lite that is being discussed to inclusion in C++20 will change the industry.